Topic: Blog post on metaprogramming
Jannis Limperg (Aug 19 2020 at 15:20):
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 (Aug 19 2020 at 19:58):
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
Last updated: May 10 2021 at 17:39 UTC