Functional Programming in Lean (leanprover.github.io)
This is an introductory book to programming in Lean 4, a pure functional language that started as a theorem prover at Microsoft Research by Leonardo de Moura. It is a dependently typed language similar to Idris, with many features inspired by Haskell....