- proof ... end
- {theorem | lemma} 名前 : 前提リスト |- 結論 proof ... end
- {fact | rule} 名前 : 前提リスト |- 結論
- we have ラベル : 命題 from 証明項
- we have ラベル : 命題 （前提または直前の結果から）
- we have 命題 {from 証明項}? （ラベルは this）
- use 証明項 （ラベルはthis）
- we propved 命題 {from 証明項} （証明内で一階しか使えない）
- it suffices to show ラベル : 命題 because the result comes from 証明項
- so we attempt to show ラベル : 命題
- assume ラベル : 命題 ... end
- postpone until 名前 （証明項の書ける場所に書ける）
- sorry {we cant}? （証明項の書ける場所に書ける）
言語的文化的習慣〈linguistic and cultural conventions〉がある。
- fact, rule とだけ書いたら、それは declare の意味になる。
- theorem, lemma とだけ書いたら、それは define の意味になる。
- define fact は許されない。define rule は許される。rule = theorem = function 。
- define opaque theorem は axiom と書いてもよい。
- 公理も declare fact, または単に fact で宣言できる。
- 入れ子になった定理は lemma と書く。
詳細：
- declare defined 外部で定義されていると宣言する。
- declare defining これからここ（モジュール）で定義することを宣言する。
- partially define 部分的な定義を与える。
- fully define 完全に定義する。デフォルト。
- 例： fully define function foo : (a:Nat) (b:Nat) |- Nat
