| 1. | Introduction |
| 2. | Elaboration and Compilation |
| 3. | The Type System |
| 4. | Interacting with Lean |
| 5. | Source Files |
| 6. | Recursive Definitions |
| 7. | Terms |
| 8. | Type Classes |
| 9. | Functors, Monads and do-Notation |
| 10. | IO |
| 11. | Tactic Proofs |
| 12. | The Simplifier |
| 13. | Basic Types |
| 14. | Standard Library |
| 15. | Notations and Macros |
| 16. | Output from Lean |
| 17. | Elan |
| 18. | Build Tools and Distribution |
| Index |