Zulip Chat Archive

Stream: general

Topic: Blog post on metaprogramming


view this post on Zulip 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!

view this post on Zulip 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 with, using, in, generalizing.


Last updated: May 10 2021 at 17:39 UTC