unification assignment

Stream: metaprogramming / tactics

[Fabian Glöckle]

Given a type target : expr and a type given : expr which unify (i.e. unify given target evaluates to tt), is it possible to retrieve the metavariable assignments made for given in the course of unification?

Reason: I would like to construct terms of type target, and do so by checking if declarations given allow one to produce such terms. To actually construct the term, I need to supply given with the correct arguments.

[Fabian Glöckle]

I.e. what I am trying to do is more or less to achieve the effect of apply given, but non-interactively.

[Jannis Limperg]

docs#tactic.apply and its variants don't do what you want?

[Fabian Glöckle]

maybe :D
I am in a tactic expr, so how would I set the main goal?

[Fabian Glöckle]

Ah, tactic.change target ff seems to be there for that

[Fabian Glöckle]

No, but then I'd get @id true ... in my proof term with tactic.result

[Fabian Glöckle]

So tactic.set_goals maybe

[Jannis Limperg]

If you just want to set the goal (to an mvar you already have lying around), set_goals.

change target requires that the main goal is defeq to target.