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.
- Introduction: the basic introduction mentioned above.
- Implementing
rw
from scratch: a tactic that does a single rewrite. - Implementing
simp
from scratch: more advanced expression manipulation.