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
?
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