Zulip Chat Archive

Stream: general

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 with, using, in, generalizing.

Last updated: Dec 20 2023 at 11:08 UTC