Functional Programming in Lean

 Functional Programming in Lean

David Thrane Christiansen

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

  1. Introduction
  2. Acknowledgments
  3. 1. Getting to Know Lean
  4. 2. Hello, World!
  5. Interlude: Propositions, Proofs, and Indexing
  6. 3. Overloading and Type Classes
  7. 4. Monads
  8. 5. Functors, Applicative Functors, and Monads
  9. 6. Monad Transformers
  10. 7. Programming with Dependent Types
  11. Interlude: Tactics, Induction, and Proofs
  12. 8. Programming, Proving, and Performance
  13. 9. Next Steps