or.elim vs or.by_cases

Stream: new members

[Thomas Brooks]

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]

docs#or.elim is for propositions only

[Thomas Brooks]

Thanks for pointing that out. Makes sense now.

[Eric Wieser]

(docs#or.by_cases for completeness)