sarahzrf (Jun 13 2020 at 14:42): sarahzrf (Jun 13 2020 at 14:42):I've been playing around with Ltac2, hoping I might be able to use it for some evil toy metaprogramming I wanted to try out, but I'm not sure if it supports the necessary features—is it just me, or is antiquotation into patterns impossible?
Pierre-Marie Pédrot (Jun 13 2020 at 20:11):Yep, it's a voluntarily omission.
Pierre-Marie Pédrot (Jun 13 2020 at 20:11):In Ltac1, terms can be antiquoted in patterns, but not patterns
Pierre-Marie Pédrot (Jun 13 2020 at 20:12):The corresponding function is known to be broken, so I'd like to have a clear understanding of the feature before implementing it
Pierre-Marie Pédrot (Jun 13 2020 at 20:12):(it's the infamous pattern_of_constr)
Pierre-Marie Pédrot (Jun 13 2020 at 20:12):(my guess is that antiquoting pattern inside patterns is rather straightforward)
sarahzrf (Jun 13 2020 at 21:34):good to know! just wish the error message were more enlightening :sweat_smile:
Last updated: Apr 19 2024 at 02:02 UTC