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?
Yep, it's a voluntarily omission.
In Ltac1, terms can be antiquoted in patterns, but not patterns
The corresponding function is known to be broken, so I'd like to have a clear understanding of the feature before implementing it
(it's the infamous
(my guess is that antiquoting pattern inside patterns is rather straightforward)
good to know! just wish the error message were more enlightening :sweat_smile:
Last updated: Jan 29 2023 at 06:02 UTC