mathlib
f23fe9a3 - doc(tactic/lean_core_docs): by_cases is classical (#3718)

Commit
5 years ago
doc(tactic/lean_core_docs): by_cases is classical (#3718) `by_cases` was changed to use classical reasoning (leanprover-community/mathlib#3354, leanprover-community/lean#409), but the documentation hasn't been updated yet. I leave `by_contra` alone as it still uses `decidable`.
Author
Parents
Loading