Stream: new members
Topic: rcases with false
Kenny Lau (Oct 02 2018 at 18:57):
Can I do
p \or false and end up with one state where we know
Reid Barton (Oct 02 2018 at 19:08):
rcases t with t'|⟨⟨⟩⟩ seems to work but I don't know if I would really advise it
Kenny Lau (Oct 02 2018 at 19:10):
would @Mario Carneiro advise it?
Simon Hudon (Oct 02 2018 at 19:13):
That looks like something I would do
Chris Hughes (Oct 02 2018 at 19:30):
or_false is a lemma. Use that.
Kenny Lau (Oct 02 2018 at 19:33):
yes. but this is just a minimal example.
Mario Carneiro (Oct 02 2018 at 23:57):
I would advise it; if you search for that (with spaces around the
| ) you will find me use it in several places
Last updated: May 08 2021 at 10:12 UTC