Setting wildcard values

Stream: new members

[Guilherme Espada]

Given an expression in my context such as a: eval ((t_abs ?m_1 ?m_2).t_app ?m_3) (upshift (-1) (subst (upshift 1 ?m_3) 0 ?m_2)) How can I fix the wildcard values? I'm currently doing it by creating another variable with the same structure and assigning a to it, but that seems sub optimal.

Thanks

[Johan Commelin]

How did they end up in that expression in the first place?

[Johan Commelin]

Those metavariables will be other goals... but it can be hard to guess which one is which.

[Guilherme Espada]

That is true, 3 subgoals seem to be produced (which disappear after I fix the variables).
Is there a simple way to manipulate the goal list? Things like sending a goal to the bottom? That would work too

[Guilherme Espada]

And yeah, would be cool if the correspondent metavar was shown in the goal. Maybe a future feature? ;)

[Johan Commelin]

swap, swap n, rotate

[Guilherme Espada]

Exactly what I was looking for, thanks!

[Guilherme Espada]

I knew about swap, but not about rotate

[Scott Morrison]

You can use use show XXX to pull a goal unifying with XXX up to the top.

[Damiano Testa]

There is also work_on_goal n. The number n begins at 0.

[Damiano Testa]

I sometimes find any_goals {tactics} and all_goals {tactics} useful.

[Guilherme Espada]

I found any_goals and all_goals very useful when working with wide inductive structures (lambda calculus)