Leanの定義構文のプロファイル部は完全なシンタックスシュガーで、無視されて、内部的にはフルカリー化版が記憶される。そそもそも、内部の還元エンジン〈reductione engine〉がフルカリー化されたポイント射しか扱えない。これが、圏論的解釈とラムダ計算的…

Lean ILean 復CCC 論理 : ⇒ → → → → [,] ⊃ 空白 :: : (なし) ∧ ∧ × ∧ true true 1 T false false 0 ⊥ 空白区切り 空白区切り カンマ区切り カンマ区切り (なし) (なし) ストリング図 横棒図 命題 命題 対象 論理式 命題リスト 命題リスト 対象リスト 論理式…

選言ボックスと二面ノード - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。絵は裏写りがすごくて、ゴミが入っていたりする。図の右下はゴミ（別な図の一部）。左から右、上から下の順で説明。 ∀elim ： ∀i∈I.A ⇒ A(a) （⇒はシーケント矢印）の証明。ケーブ…