Commit 2024-09-13 20:11 bb7a63b1

View on Github →

chore: deprecate Ordering.orElse for .then (#12068) Ordering.orElse is a duplicate of Ordering.then from Init. Similarly, toRel is a duplicate of Compares. (cmp is also a duplicate of compareOfLessAndEq, but it's used quite heavily and the new name is a bit...)

Estimated changes

Modified Mathlib/Data/Ordering/Basic.lean

added def Ordering.Compares

added theorem Ordering.compares_eq

added theorem Ordering.compares_gt

added theorem Ordering.compares_lt

deleted def Ordering.orElse

deleted def Ordering.toRel

Modified Mathlib/Order/Compare.lean

deleted def Ordering.Compares

deleted theorem Ordering.compares_eq

deleted theorem Ordering.compares_gt

deleted theorem Ordering.compares_lt

modified theorem Ordering.orElse_eq_lt

modified theorem Ordering.swap_orElse

Modified Mathlib/Order/Defs.lean

modified theorem compare_iff

Modified Mathlib/SetTheory/Ordinal/Notation.lean