Functional Programming in Lean
Copyright Microsoft Corporation 2023 and Lean FRO, LLC 2023–2025
This is a free book on using Lean as a programming language. All code samples are tested with Lean release 4.18.0.
Contents
- Introduction
- Acknowledgments
- 1. Getting to Know Lean
- 2. Hello, World!
- Interlude: Propositions, Proofs, and Indexing
- 3. Overloading and Type Classes
- 4. Monads
- 5. Functors, Applicative Functors, and Monads
- 6. Monad Transformers
- 7. Programming with Dependent Types
- Interlude: Tactics, Induction, and Proofs
- 8. Programming, Proving, and Performance
- 9. Next Steps