Commit 2020-08-15 20:41 7f1a4893

View on Github →

fix(algebra/order): restore choiceless theorems (#3799) The classical_decidable linter commit made these choiceless proofs use choice again, making them duplicates of other theorems not in the decidable. namespace.

Estimated changes

Modified src/algebra/order.lean

modified theorem decidable.eq_or_lt_of_le

modified theorem decidable.le_iff_le_iff_lt_iff_lt

modified theorem decidable.le_iff_lt_or_eq

modified theorem decidable.le_imp_le_iff_lt_imp_lt

modified theorem decidable.le_imp_le_of_lt_imp_lt

modified theorem decidable.le_of_not_lt

modified theorem decidable.le_or_lt

modified theorem decidable.lt_or_eq_of_le

modified theorem decidable.lt_or_gt_of_ne

modified theorem decidable.lt_or_le

modified theorem decidable.lt_trichotomy

modified theorem decidable.ne_iff_lt_or_gt

modified theorem decidable.not_lt