Tutorials
These tutorials cover version 4.27.0-rc1 of Lean. While the reference manual describes the system and its features in detail, these tutorials introduce one specific aspect.
Tactics
These tutorials demonstrate Lean's advanced proof automation.
- Verifying Imperative Programs Using
mvcgen A demonstration of how to use Lean's verification condition generator to conveniently and compositionally prove properties of monadic programs.
- Using
grindfor Ordered Maps A demonstration of how to use `grind` to automate essentially all proofs in a new data structure, with an interface that finds proofs automatically.