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