The documentation says that in a match statement, Ltac2 ?id variables will only bind to closed terms. That makes sense, but then how should we match an open term?

For example, suppose I have `forall x : A,N `

and `M`

which is closed. I want to decide whether `M`

unifies (or is syntactically identical) with `N`

for the appropriate instantation of `x`

. Intuitively the way I would think to do this is by constructing a pattern `N[x/?y]`

, where the free variable `y`

is replaced with an Ltac2 variable, and we then try to unify this pattern with `M`

, but this seems incompatible with `?id`

only binding closed terms as we can't get `N[x/?y]`

easily to begin with.

I will give a more concrete example. Say I know `forall x. A(x) -> B(x)`

and I want to write a tactic which replaces all occurrences `A`

with `B`

in the hypothesis. Say I have a hypothesis `forall x1 x2... xn, A(t(x1,... xn))`

and I want to replace it with `forall x1 x2 ... xn, B(t(x1,... xn))`

. How can I check that `A(t(x1,...xn))`

is unifiable with `A(x)`

in order to decide which ones I should try this on?

Last updated: Oct 12 2024 at 12:01 UTC