Def Ordering.orElse

Modification history

2024-09-13 20:11

Mathlib/Data/Ordering/Basic.lean

chore: deprecate `Ordering.orElse` for `.then` (#12068) …

Deleted Ordering.orElse View on Github →

2022-11-11 02:27

Mathlib/Init/Data/Ordering/Basic.lean

feat: Init.Data.Ordering.Basic (#568)

Added Ordering.orElse View on Github →