| 1. | Introduction |
| 2. | Elaboration and Compilation |
| 3. | The Type System |
| 4. | Source Files |
| 5. | Recursive Definitions |
| 6. | Terms |
| 7. | Type Classes |
| 8. | 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. | Build Tools and Distribution |
| Index |