Introduction to Tactic Writing in Lean

Originally, this was a single Lean file, later we extended the tutorial with further files with more advanced topics.

If you are a metaprogramming beginner, we recommend to start with TacticProgrammingGuide.lean. There are 762 lines coverging the basics of Lean tactic writing. We assume you already know Lean, and probably use VS Code, in that case clone this repository, or simply download the file.

Alternatively, you can also copy it to Lean 4 Web but you will miss the Ctrl-click feature.

We tried to explain all the basic concepts but keep at least the introduction it beginner friendly. Enjoy learning Lean metaprogramming. If you are getting confused somewhere, it is probably not your fault. Let us know what needs more clarification in the Zulip thread.

Content

So far, there are three tutorials of increasing difficulty. Although you can scroll through it on Github, we indeed recommend to download the files and play with them.