Zulip Chat Archive

Stream: Is there code for X?

Topic: Switch current goal based on pattern


Dylan Ede (May 07 2021 at 13:53):

I'm only just beginning with Lean, so I'm probably missing something obvious, but how do I switch the current goal to the one matching a given pattern?

Eric Wieser (May 07 2021 at 13:53):

Can you give a #mwe?

Eric Wieser (May 07 2021 at 13:55):

Are you describing a case similar to having three goals x = 0, y = 0, and x + y = z, and you want to work on the y = 0 goal first?

Eric Wieser (May 07 2021 at 13:55):

If so that's tactic#show

Dylan Ede (May 07 2021 at 13:59):

Yes, exactly. I had tried that before but thought it didn't work. Now I see that my actual problem was that the pattern I gave matched both goals. D'oh!


Last updated: Dec 20 2023 at 11:08 UTC