inductive Eq : α → α → Prop where
/-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the
equality type. See also `rfl`, which is usually used instead. -/
| refl (a : α) : Eq a a
/-
recursor Eq.rec.{u, u_1} : {α : Sort u_1} →
{a : α} → {motive : (a_1 : α) → a = a_1 → Sort u} → motive a (_ : a = a) → {a_1 : α} → (t : a = a_1) → motive a_1 t
-/Eq.recを見やすく書き換える。
Eq.rec
|-
{α : Sort u_1} →
{a : α} →
{motive : (a_1 : α) → a = a_1 → Sort u} →
motive a (_ : a = a) →
{a_1 : α} →
(t : a = a_1) → motive a_1 tつまり：
Eq.rec
{α : Sort u_1}
{a : α}
{motive : (a_1 : α) → a = a_1 → Sort u}
|-
motive a (_ : a = a) →
({a_1 : α} → (t : a = a_1) → motive a_1 t)Eq.recの中置演算子記号が 「▸（U+25b8 BLACK RIGHT-POINTING SMALL TRIANGLE）」となる。
def toNum (b : Bool) : Nat := by cases b with | true => exact 1 | false => exact 0 #print toNum #print Bool.casesOn
InfoViewの表示
def toNum : Bool → Nat :=
fun b =>
Bool.casesOn (motive := fun t => b = t → Nat) b (fun h => (_ : false = b) ▸ 0) (fun h => (_ : true = b) ▸ 1)
(_ : b = b)
@[reducible] protected def Bool.casesOn.{u} : {motive : Bool → Sort u} →
(t : Bool) → motive false → motive true → motive t :=
fun {motive} t false true => Bool.rec false true t
