There is a short one[1] from Functional Programming in Lean, which is itself an introduction to Lean 4 from the programming's perspective. Highly recommended if

There is a short one[1] from Functional Programming in Lean, which is itself an introduction to Lean 4 from the programming's perspective. Highly recommended if you're interested in dependent types. [1]: https://leanprover.github.io/functional_programming_in_lean/introduction.html https://leanprover.github.io/functional_programming_in_lean/...