Zulip Chat Archive

Stream: new members

Topic: or.elim vs or.by_cases


Thomas Brooks (Feb 06 2022 at 16:13):

What's the difference between or.elim and or.by_cases? It seems like by_cases requires two decidable Props and or.elim doesn't and they give the same result. So why ever use or.by_cases?

Reid Barton (Feb 06 2022 at 16:26):

docs#or.elim is for propositions only

Thomas Brooks (Feb 06 2022 at 16:51):

Thanks for pointing that out. Makes sense now.

Eric Wieser (Feb 06 2022 at 22:05):

(docs#or.by_cases for completeness)


Last updated: Dec 20 2023 at 11:08 UTC