Zulip Chat Archive

Stream: new members

Topic: Setting wildcard values


view this post on Zulip Guilherme Espada (Mar 17 2021 at 16:57):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 17:23):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 17:23):

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

view this post on Zulip Guilherme Espada (Mar 17 2021 at 17:28):

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

view this post on Zulip Guilherme Espada (Mar 17 2021 at 17:28):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 17:46):

swap, swap n, rotate

view this post on Zulip Guilherme Espada (Mar 17 2021 at 18:38):

Exactly what I was looking for, thanks!

view this post on Zulip Guilherme Espada (Mar 17 2021 at 18:38):

I knew about swap, but not about rotate

view this post on Zulip Scott Morrison (Mar 17 2021 at 22:33):

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

view this post on Zulip Damiano Testa (Mar 18 2021 at 05:17):

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

view this post on Zulip Damiano Testa (Mar 18 2021 at 05:19):

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

view this post on Zulip Guilherme Espada (Mar 18 2021 at 11:10):

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


Last updated: May 06 2021 at 21:09 UTC