Introduction to tactic programming

Stream: new members

[Mirek Olšák]

Cross-posting from metaprogramming / tactics

Mirek Olšák said:

Inspired by discussions on BigProof, we wrote an introduction to tactic programming with Jovan Gerbscheid , also thanks Anand Rao Tadipatri for checking early version.
https://github.com/mirefek/lean-tactic-programming-guide
If you are a Lean user interested in how tactics work, and how you could one day write your own, we would love to hear your feedback!
(of course we are also curious about critique from experts)