Stream: Coq users

Topic: Ltac2 pattern stuff


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

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 20:11):

Yep, it's a voluntarily omission.

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 20:11):

In Ltac1, terms can be antiquoted in patterns, but not patterns

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

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 20:12):

(it's the infamous pattern_of_constr)

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 20:12):

(my guess is that antiquoting pattern inside patterns is rather straightforward)

view this post on Zulip sarahzrf (Jun 13 2020 at 21:34):

good to know! just wish the error message were more enlightening :sweat_smile:


Last updated: Jan 29 2023 at 06:02 UTC