Zulip Chat Archive

Stream: new members

Topic: rcases with false


view this post on Zulip Kenny Lau (Oct 02 2018 at 18:57):

Can I do rcases on p \or false and end up with one state where we know p?

view this post on Zulip Reid Barton (Oct 02 2018 at 19:08):

Well rcases t with t'|⟨⟨⟩⟩ seems to work but I don't know if I would really advise it

view this post on Zulip Kenny Lau (Oct 02 2018 at 19:10):

would @Mario Carneiro advise it?

view this post on Zulip Simon Hudon (Oct 02 2018 at 19:13):

That looks like something I would do

view this post on Zulip Chris Hughes (Oct 02 2018 at 19:30):

I'm sure or_false is a lemma. Use that.

view this post on Zulip Kenny Lau (Oct 02 2018 at 19:33):

yes. but this is just a minimal example.

view this post on Zulip 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