Zulip Chat Archive

Stream: new members

Topic: the order of goals

Alex Zhang (Jul 20 2021 at 21:21):

If I have several goals in an info view, how can I choose a goal to do first?

Adam Topaz (Jul 20 2021 at 21:22):

tactic#show or tactic#swap

Kevin Buzzard (Jul 20 2021 at 21:23):

You shouldn't have several goals in scope though, it makes your code much harder to read. Use { } to keep your number of goals down to 1.

Alex Zhang (Jul 20 2021 at 21:25):

I mean, if I have two goals, use {} will automatically choose the first.

Eric Wieser (Jul 20 2021 at 21:26):

Do you have a reason for not wanting to solve that goal first? If you just don't want to solve it right now, you can use { sorry }, to put it off till later

Eric Wieser (Jul 20 2021 at 21:27):

The only other situation I can think of is when the first goal has metavariables that you want to fill in - but usually there's a way to get the goals in the right order to start with in those cases.

Yakov Pechersky (Jul 20 2021 at 21:36):

Even if the second has metavariables, it is likely solvable

Mario Carneiro (Jul 20 2021 at 21:58):

case is also a good way to select goals, especially after induction, which will label the goals

Mario Carneiro (Jul 20 2021 at 21:58):

swap n will bring the nth goal to the front

Mario Carneiro (Jul 20 2021 at 21:59):

work_on_goal n will apply a tactic to the nth goal

Mario Carneiro (Jul 20 2021 at 22:00):

finally tac; [skip, skip, tac2] can be used to different tactics to the goals coming out of another tactic

Eric Wieser (Jul 20 2021 at 22:03):

rotate hadn't been mentioned yet

Last updated: Dec 20 2023 at 11:08 UTC