missing manual chapters

Stream: new members

[Michael Beeson]

The Lean Reference Manual's table of contents announces chapters on programming, metaprogramming, and libraries that do not actually exist. So how can I learn to write my own tactics?

[Jalex Stark]

you can ask questions here and in the metaprogramming stream, you can read the source code of tactics in mathlib

[Rob Lewis]

Also see @Patrick Massot 's tutorial at https://leanprover-community.github.io/extras/tactic_writing.html

[Marc Huisinga]

additional resources:

• https://leanprover.github.io/papers/tactic.pdf
• chapter 6 and 7 of the hitchhiker's guide to logical verification (https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf)

[Rob Lewis]

I was looking for the link to the Hitchhiker's Guide but you beat me to it. That's probably the most in depth writeup I know of.

[Patrick Massot]

I was about to write that https://leanprover-community.github.io/learn.html has a section dedicated to meta-programming but the HH guide is missing there.

[Patrick Massot]

I'll fix it

[Patrick Massot]

Fixed