Functional Programming in Lean – an in-progress book
leanprover.github.io