イコールのリカーサーと黒三角演算子記号

Lean

Eq〈イコール〉の定義：

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

この定義のリカーサー〈帰納原理〉が Eq.rec になる。Eq.recの中置演算子記号が 「▸（U+25b8 BLACK RIGHT-POINTING SMALL TRIANGLE）▸」となる。

  • h₁ ▸ h₂ ▸ rfl ≡ Eq.rec (Eq.rec rfl h₂) h
/-
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のリカーサーちゃんと理解しないとな。