Zulip Chat Archive

Stream: lean4

Topic: Typed Macros

Sebastian Ullrich (Jun 24 2022 at 21:38):

PR just dropped: https://github.com/leanprover/lean4/pull/1251
Feel free to ask question or discuss here if you prefer

Henrik Böving (Jun 24 2022 at 21:45):

Am I understanding correctly that macro and the likes will use TSyntax per default from now on without any change/flag/w/e from the user?

Sebastian Ullrich (Jun 24 2022 at 21:49):

Basically yes (technically no, see Ctrl+F "technically"), but also see use of open TSyntax.Compat in to ease/postpone porting of old code to some degree

Sebastian Ullrich (Jun 24 2022 at 21:53):

Anyway, for new/adapted code making use of quotations, this should remove almost all sources of ill-formed syntax tree bugs, yes

Henrik Böving (Jun 24 2022 at 21:58):

What a great coincidence I delayed describing those in the meta book up until now then :p

Last updated: Dec 20 2023 at 11:08 UTC