Zulip Chat Archive

Stream: lean4

Topic: help reducing duplicated code


Jesse Slater (Jan 11 2023 at 18:12):

I am doing a proof by cases with a match statement , and three of my cases have exactly the same proof. However, I can't figure out how to combine it and only write that proof once.
image.png

I tried using wildcards, but that did not work.
image.png

The match does recognize that these are the three cases that need to be solved if I omit them.
image.png

Marcus Rossel (Jan 11 2023 at 18:16):

Could you post a #mwe? Also, images are a bit annoying to work with for people trying to give solutions - try #backticks.

Chris Bailey (Jan 11 2023 at 21:57):

Try this syntax:

| 1, 0 | 0, 1 | 0, 0 => /- your proof -/

Jesse Slater (Jan 12 2023 at 14:12):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC