Stream: Ltac2

Topic: Constr binders


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

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

view this post on Zulip Pierre-Marie Pédrot (Feb 01 2022 at 17:29):

You should match on the constr inside the branch to retrieve the name.

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

view this post on Zulip 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: Jan 31 2023 at 11:01 UTC