Blog post on metaprogramming

Stream: general

[Jannis Limperg]

I wrote a little post on some of Lean's metaprogramming gotchas and how to get around them. None of this is new, but I hope that novice metaprogrammers will find some useful info on how to deal with the idiosyncrasies of Lean's API. Feedback and corrections very welcome!

[Mario Carneiro]

In 5.1, it is worth mentioning that if you declare an identifier as a token using the precedence command, then it can never again be used as a local variable name or function name. That is why most tactics use and reuse a relatively poor vocabulary of filler words like with, using, in, generalizing.