#print で既存の帰納型を紹介しない

LeanByExample/Reference/Tactic/Cases.lean

@@ -44,22 +44,7 @@ example : P ∨ Q → (P → R) → (Q → R) → R := by
 /- ## 舞台裏
 
 `cases` は、実際には論理和に限らず[帰納型](../Declarative/Inductive.md)をコンストラクタに分解することができるタクティクです。
-論理和を分解することができるのも、`Or` が帰納型として定義されているからです。
 -/
-namespace Cases --#
-
-/--
-info: inductive Or : Prop → Prop → Prop
-number of parameters: 2
-constructors:
-Or.inl : ∀ {a b : Prop}, a → a ∨ b
-Or.inr : ∀ {a b : Prop}, b → a ∨ b
--/
-#guard_msgs in #print Or
-
--- Or のコンストラクタ
-#check (Or.inl : P → P ∨ Q)
-#check (Or.inr : Q → P ∨ Q)
 
 -- 帰納型として定義した例示のための型
 inductive Sample where
@@ -76,4 +61,23 @@ example (s : Sample) : True := by
   case bar z =>
     trivial
 
+/- 論理和を分解することができるのも、`Or` が次のように帰納型として定義されているからです。 -/
+namespace Cases --#
+
+--#--
+-- Or の定義が変わっていないことを確認するためのコード
+/--
+info: inductive Or : Prop → Prop → Prop
+number of parameters: 2
+constructors:
+Or.inl : ∀ {a b : Prop}, a → a ∨ b
+Or.inr : ∀ {a b : Prop}, b → a ∨ b
+-/
+#guard_msgs in #print Or
+--#--
+
+inductive Or (a b : Prop) : Prop where
+  | inl (h : a) : Or a b
+  | inr (h : b) : Or a b
+
 end Cases --#

LeanByExample/Reference/Tactic/Exists.lean

@@ -5,28 +5,28 @@
 ゴールが `⊢ ∃ x, P x` のとき、`x: X` がローカルコンテキストにあれば、`exists x` によりゴールが `P x` に変わります。同時に、`P x` が自明な場合は証明が終了します。-/
 import Lean --#
 
-namespace Exists --#
-
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
   exists 2
 
 /- ## 内部処理についての補足
 なお Lean での存在量化の定義は次のようになっています。-/
-
-universe u
-
+--#--
+-- Exists の定義が変わっていないことを確認する
 /--
 info: inductive Exists.{u} : {α : Sort u} → (α → Prop) → Prop
 number of parameters: 2
 constructors:
 Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
 -/
 #guard_msgs in #print Exists
+--#--
+namespace Exists --#
 
--- `p : α → Prop` は `α` 上の述語とする。
--- このとき `w : α` と `h : p w` が与えられたとき `∃ x : α, p x` が成り立つ。
-#check (Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α) (_h : p w), Exists p)
+inductive Exists.{u} {α : Sort u} (p : α → Prop) : Prop where
+  /-- `a : α` と `h : p a` から `∃ x : α, p x` の証明を得る -/
+  | intro (w : α) (h : p w) : Exists p
 
+end Exists --#
 /- したがって `Exists` は単一のコンストラクタを持つ[帰納型](../Declarative/Inductive.md)、つまり[構造体](../Declarative/Structure.md)なので、上記の `exists` は `exact` と[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/
 
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
@@ -56,5 +56,3 @@ elab "#expand " t:macro_stx : command => do
 /-- info: (refine ⟨1, 2, 3, ?_⟩; try trivial) -/
 #guard_msgs in
   #expand exists 1, 2, 3
-
-end Exists --#

LeanByExample/Reference/TypeClass/Decidable.lean

@@ -46,6 +46,8 @@ example : Even 4 := by decide
 /- ## class inductive
 `Decidable` 型クラスの定義は少し特殊です。コンストラクタが複数あり、[構造体](../Declarative/Structure.md)ではなく[帰納型](../Declarative/Inductive.md)の構造をしています。これは `Decidable` が [`class inductive`](../Declarative/Class.md#ClassInductive) というコマンドで定義されているためです。-/
 
+--#--
+-- Decidable の定義が変わっていないことを確認する
 /--
 info: inductive Decidable : Prop → Type
 number of parameters: 1
@@ -54,5 +56,12 @@ Decidable.isFalse : {p : Prop} → ¬p → Decidable p
 Decidable.isTrue : {p : Prop} → p → Decidable p
 -/
 #guard_msgs in #print Decidable
+--#--
+
+class inductive Decidable (p : Prop) where
+  /-- `¬ p` であることが分かっているなら、`p` は決定可能 -/
+  | isFalse (h : Not p) : Decidable p
+  /-- `p` であることが分かっているなら、`p` は決定可能 -/
+  | isTrue (h : p) : Decidable p
 
 end Decidable --#