| 1. | Introduction |
| 2. | Elaboration and Compilation |
| 3. | Interacting with Lean |
| 4. | The Type System |
| 5. | Source Files and Modules |
| 6. | Namespaces and Sections |
| 7. | Definitions |
| 8. | Axioms |
| 9. | Attributes |
| 10. | Terms |
| 11. | Type Classes |
| 12. | Coercions |
| 13. | Tactic Proofs |
| 14. | Functors, Monads and do-Notation |
| 15. | IO |
| 16. | The Simplifier |
| 17. | Basic Propositions |
| 18. | Basic Types |
| 19. | Notations and Macros |
| 20. | Run-Time Code |
| 21. | Build Tools and Distribution |
| Release Notes |
| Index |
