Functional Programming in Lean
All code samples are tested with Lean 4 release nightly-2023-05-22. This is the last release prior to the final release. This release adds a chapter on programming with dependent types and indexed families. The December 2022 release was delayed until January 2023 due to winter holidays. This release adds a chapter on programming with monads. This release adds the first half of a chapter on type classes, which are Lean's mechanism for overloading operators and an important means of organizing code and structuring libraries. The second public release completes the first chapter.