Helper definitions and instances for Ordering

instance instReprOrdering_mathlib : Repr Ordering

Equations

• instReprOrdering_mathlib = { reprPrec := reprOrdering✝ }

@[deprecated Ordering.then]

def Ordering.orElse : Ordering → Ordering → Ordering

Alias of Ordering.then.

---

If o₁ and o₂ are Ordering, then o₁.then o₂ returns o₁ unless it is .eq, in which case it returns o₂. Additionally, it has "short-circuiting" semantics similar to boolean x && y: if o₁ is not .eq then the expression for o₂ is not evaluated. This is a useful primitive for constructing lexicographic comparator functions:

structure Person where
  name : String
  age : Nat

instance : Ord Person where
  compare a b := (compare a.name b.name).then (compare b.age a.age)

This example will sort people first by name (in ascending order) and will sort people with the same name by age (in descending order). (If all fields are sorted ascending and in the same order as they are listed in the structure, you can also use deriving Ord on the structure definition for the same effect.)

Equations

• Ordering.orElse = Ordering.then

def Ordering.Compares {α : Type u_1} [LT α] : Ordering → α → α → Prop

Compares o a b means that a and b have the ordering relation o between them, assuming that the relation a < b is defined.

Equations

• Ordering.lt.Compares x✝ x = (x✝ < x)
• Ordering.eq.Compares x✝ x = (x✝ = x)
• Ordering.gt.Compares x✝ x = (x✝ > x)

@[deprecated Ordering.Compares]

def Ordering.toRel {α : Type u_1} [LT α] : Ordering → α → α → Prop

Alias of Ordering.Compares.

---

Compares o a b means that a and b have the ordering relation o between them, assuming that the relation a < b is defined.

Equations

• @Ordering.toRel = @Ordering.Compares

@[simp]

theorem Ordering.compares_lt {α : Type u_1} [LT α] (a b : α) : Ordering.lt.Compares a b = (a < b)

@[simp]

theorem Ordering.compares_eq {α : Type u_1} [LT α] (a b : α) : Ordering.eq.Compares a b = (a = b)

@[simp]

theorem Ordering.compares_gt {α : Type u_1} [LT α] (a b : α) : Ordering.gt.Compares a b = (a > b)

def cmpUsing {α : Type u} (lt : α → α → Prop) [DecidableRel lt] (a b : α) : Ordering

Lift a decidable relation to an Ordering, assuming that incomparable terms are Ordering.eq.

Equations

• cmpUsing lt a b = if lt a b then Ordering.lt else if lt b a then Ordering.gt else Ordering.eq

def cmp {α : Type u} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (a b : α) : Ordering

Construct an Ordering from a type with a decidable LT instance, assuming that incomparable terms are Ordering.eq.

Equations

• cmp a b = cmpUsing (fun (x1 x2 : α) => x1 < x2) a b