Guillaume Melquiond (Feb 01 2022 at 15:56): Guillaume Melquiond (Feb 01 2022 at 15:56):I am trying to recover the name of a binder, so that I can later pass it to Fresh.in_goal, for example. But the desugared output of the following snippet makes me think it is impossible. Is that right?
Ltac2 foo h := lazy_match! h with | forall x : ?t, _ => () end.
Just in case, I tried to replace x with ?x, but then I get a syntax error.
Do I need to write my own version of match! using the primitives of Constr?
Pierre-Marie Pédrot (Feb 01 2022 at 17:29):This is explicitly designed to not handle this because the whole Ltac name matching is completely broken if you think a bit about it (it's both a binder in the patter and a metabinder outside)
Pierre-Marie Pédrot (Feb 01 2022 at 17:29):You should match on the constr inside the branch to retrieve the name.
Pierre-Marie Pédrot (Feb 01 2022 at 17:30):(IIRC the low-level match function still gives you access to the names but then you're on your own there)
Guillaume Melquiond (Feb 01 2022 at 17:38):I don't care whether it is broken. If the user bothered to give a name to a binder, I want to be able to produce a binder with the same name. Because, let us be honest, Coq's automatic naming of binders is even more broken.
Last updated: Apr 16 2024 at 21:01 UTC