Leanのキーワード

とりあえず、Leandで使っているキーワード。

証明には限らないモノ。

1. コメント -- （ハイフン2個、行末まで）
2. コメント /- -/
3. ==> ラムダ記法の一部、ピリオド相当
4. fun 〈λ〉
5. def :=
6. let := ; （ローカル定義、in ではなくて ;）
7. variable （変数の予約）
8. section end （名前のスコープ）
9. namespace end （名前のスコープ）
10. open 名前空間 （名前をばらまく）
11. universe （宇宙レベルの宣言）
12. { } （暗黙引数）
13. example （def と同じようだ）

証明で使うモノ。

1. Prop （命題の宇宙）
2. axiom （命題に証明を対応させる関数の宣言用）
3. therem （命題に証明を対応させる関数の定義用）
4. show p from r （showは特に何もしないアノテーション、from は根拠となる導出射を示す）
5. have ？？
6. by 根拠となるタクティク