Retrieving interactively constructed terms

Stream: general

[Seul Baek]

Suppose I'd like to construct a term of type τ interactively, so I use e ← assert n '(τ) and apply some further tactics to close off the goal. Now e is bound to a local constant, which is the expr of a term that has type τ.

Later in the proof, I need to call a tactic foo : τ → tactic unit. I think I should be able to use e in some way to extract a term t : τ to be used as an argument for foo. But t ← eval_expr τ e doesn't work, because eval_expr only works on closed expressions. Is there something else I can do to retrieve the constructed term?

It seems that define retains more information than assert, but I'm not sure whether that helps.

[Sebastian Ullrich]

You should probably use tactic.solve_aux in favor of assert

[Seul Baek]

@Sebastian Ullrich I think this is closer to what I need, but it requires that you provide upfront a specific tactic which will solve the newly created goal. If there is a need to go interactive because it can't be predicted beforehand which tactic will do the job, I wonder if there are alternatives?

I'm currently experimenting with combinations of assert and mk_meta_var, but it seems that anything I do will only add a local constant to the context, instead of the actual term. Perhaps I'm trying to do something that you're not supposed to do :confused:

[Sebastian Ullrich]

If there is a need to go interactive because it can't be predicted beforehand which tactic will do the job, I wonder if there are alternatives?

I'm not sure I understand, what does your use case look like that you don't know when the goal will be solved? Anyway, if you copy and adapt solve_aux's implementation, you should be able to do something like that.