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, but then I get a syntax error.
Do I need to write my own version of
match! using the primitives of
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)
You should match on the constr inside the branch to retrieve the name.
(IIRC the low-level match function still gives you access to the names but then you're on your own there)
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: Dec 05 2023 at 06:01 UTC