Functional Programming in Lean

by David Thrane Christiansen

This is an in-progress book on using Lean 4 as a programming language. The most recent release is found at, and it will be updated monthly. This version of the text is written for Lean version 4.0.0-nightly-2022-06-04, commit a65197bb785a.

Release history

June, 2022

This was the first public release, consisting of an introduction and part of the first chapter.

About the Author

David Thrane Christiansen has been using functional languages for twenty years, and dependent types for ten. Together with Daniel P. Friedman, he wrote The Little Typer, an introduction to the key ideas of dependent type theory. He has a Ph.D. from the IT University of Copenhagen. During his studies, he was a major contributor to the first version of the Idris language. Since leaving academia, he has worked at Galois in Portland, Oregon and Deon Digital in Copenhagen, Denmark. At the time of writing, he is the Executive Director of the Haskell Foundation.