A new release of Functional Programming in Lean is out! https://leanprover.github.io/functional_programming_in_lean/
The new chapter this time around focuses on programming with dependent types.
@prozacchiwawa The next chapter may be just what you've been waiting for
@d_christiansen im overdue to try writing some lean again. maybe i can figure out how to convince it my function was total after all.