1. | はじめに(Introduction) |
2. | エラボレーションとコンパイル(Elaboration and Compilation) |
3. | 型システム(The Type System) |
4. | ソースファイル(Source Files) |
5. | 再帰定義(Recursive Definitions) |
6. | 項(Terms) |
7. | 型クラス(Type Classes) |
8. | 関手・モナド・do記法(Functors, Monads and do -Notation) |
9. | IO |
10. | タクティクによる証明(Tactic Proofs) |
11. | 単純化器(The Simplifier) |
12. | 基本的な型(Basic Types) |
13. | Standard Library |
14. | 記法とマクロ(Notations and Macros) |
15. | Output from Lean |
16. | Elan |
17. | Lake and Reservoir |
| Index |
18. | この翻訳について |