Programing Refrences

Stream: general

[Christopher Upshaw]

So what are some good places to read up on Lean 3/4 specifically as a programing language, as opposed to using it for mathematics? I hang out on the mathlib discord server so I know lots about it as a prover.

[Bryan Gin-ge Chen]

The only resources specific to Lean (3) I know of are in the "tactic writing and metaprogramming" section of our Learning resources page.

[Jason Rute]

For lean 3: https://agentultra.github.io/lean-for-hackers/

[Jason Rute]

For lean 4, see the manual: https://leanprover.github.io/lean4/doc/

[Jason Rute]

Lean 4 is designed to be a useable programming language. Lean 3’s programming language is harder to use IMHO and mostly used for metaprogramming (writing tactics and other code to inspect internal lean objects).

[Jason Rute]

If you are not familiar with the basics of monads, you can find good introductions on the internet by Googling. Also this is a good intro for monads in Lean although it might be really outdated.

[Jason Rute]

https://avigad.github.io/programming_in_lean/monads.html