LeanLangur

This is a repository where I am gathering all the material I use for talks and demos in Lean. I am also working to make this a partly self-contained, programming focussed introduction to Lean.

Using the repository

There are many excellent resources for learning how to prove using tactics in Lean, so I will not duplicate this. Specifically, I strongly recommend Patrick Massot's A glimpse of Lean. It will be assumed that you have worked the Exercises and done at least one topic there, or you have learned Lean to that level from some other source.

To use this repository, start with the README of the sub-directory LeanLangur. This gives an outline of files and their dependencies.

About the name

This continued my series of (ideally alliterative) local animal names, starting with LeanLion in Singapore. There is an accidental pun - the name can be parsed as LeanLang-ur, the town/city of LeanLang.