Init.Data.Ord

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.eq.then b = b
a.then b = a

source

def Ordering.isEq :

Ordering → Bool

Check whether the ordering is 'equal'.

Equations

Ordering.eq.isEq = true
x✝.isEq = false

source

def Ordering.isNe :

Ordering → Bool

Check whether the ordering is 'not equal'.

Equations

Ordering.eq.isNe = false
x✝.isNe = true

source

def Ordering.isLE :

Ordering → Bool

Check whether the ordering is 'less than or equal to'.

Equations

Ordering.gt.isLE = false
x✝.isLE = true

source

def Ordering.isLT :

Ordering → Bool

Check whether the ordering is 'less than'.

Equations

Ordering.lt.isLT = true
x✝.isLT = false

source

def Ordering.isGT :

Ordering → Bool

Check whether the ordering is 'greater than'.

Equations

Ordering.gt.isGT = true
x✝.isGT = false

source

def Ordering.isGE :

Ordering → Bool

Check whether the ordering is 'greater than or equal'.

Equations

Ordering.lt.isGE = false
x✝.isGE = true

source

@[simp]

theorem Ordering.isLT_lt :

lt.isLT = true

source

@[simp]

theorem Ordering.isLE_lt :

lt.isLE = true

source

@[simp]

theorem Ordering.isEq_lt :

lt.isEq = false

source

@[simp]

theorem Ordering.isNe_lt :

lt.isNe = true

source

@[simp]

theorem Ordering.isGE_lt :

lt.isGE = false

source

@[simp]

theorem Ordering.isGT_lt :

lt.isGT = false

source

@[simp]

theorem Ordering.isLT_eq :

eq.isLT = false

source

@[simp]

theorem Ordering.isLE_eq :

eq.isLE = true

source

@[simp]

theorem Ordering.isEq_eq :

eq.isEq = true

source

@[simp]

theorem Ordering.isNe_eq :

eq.isNe = false

source

@[simp]

theorem Ordering.isGE_eq :

eq.isGE = true

source

@[simp]

theorem Ordering.isGT_eq :

eq.isGT = false

source

@[simp]

theorem Ordering.isLT_gt :

gt.isLT = false

source

@[simp]

theorem Ordering.isLE_gt :

gt.isLE = false

source

@[simp]

theorem Ordering.isEq_gt :

gt.isEq = false

source

@[simp]

theorem Ordering.isNe_gt :

gt.isNe = true

source

@[simp]

theorem Ordering.isGE_gt :

gt.isGE = true

source

@[simp]

theorem Ordering.isGT_gt :

gt.isGT = true

source

@[simp]

theorem Ordering.swap_lt :

lt.swap = gt

source

@[simp]

theorem Ordering.swap_eq :

eq.swap = eq

source

@[simp]

theorem Ordering.swap_gt :

gt.swap = lt

source

theorem Ordering.eq_eq_of_isLE_of_isLE_swap {o : Ordering} :

o.isLE = true → o.swap.isLE = true → o = eq

source

theorem Ordering.eq_eq_of_isGE_of_isGE_swap {o : Ordering} :

o.isGE = true → o.swap.isGE = true → o = eq

source

theorem Ordering.eq_eq_of_isLE_of_isGE {o : Ordering} :

o.isLE = true → o.isGE = true → o = eq

source

theorem Ordering.eq_swap_iff_eq_eq {o : Ordering} :

o = o.swap ↔ o = eq

source

theorem Ordering.eq_eq_of_eq_swap {o : Ordering} :

o = o.swap → o = eq

source

@[simp]

theorem Ordering.isLE_eq_false {o : Ordering} :

o.isLE = false ↔ o = gt

source

@[simp]

theorem Ordering.isGE_eq_false {o : Ordering} :

o.isGE = false ↔ o = lt

source

@[simp]

theorem Ordering.swap_eq_gt {o : Ordering} :

o.swap = gt ↔ o = lt

source

@[simp]

theorem Ordering.swap_eq_lt {o : Ordering} :

o.swap = lt ↔ o = gt

source

@[simp]

theorem Ordering.swap_eq_eq {o : Ordering} :

o.swap = eq ↔ o = eq

source

@[simp]

theorem Ordering.isLT_swap {o : Ordering} :

o.swap.isLT = o.isGT

source

@[simp]

theorem Ordering.isLE_swap {o : Ordering} :

o.swap.isLE = o.isGE

source

@[simp]

theorem Ordering.isEq_swap {o : Ordering} :

o.swap.isEq = o.isEq

source

@[simp]

theorem Ordering.isNe_swap {o : Ordering} :

o.swap.isNe = o.isNe

source

@[simp]

theorem Ordering.isGE_swap {o : Ordering} :

o.swap.isGE = o.isLE

source

@[simp]

theorem Ordering.isGT_swap {o : Ordering} :

o.swap.isGT = o.isLT

source

theorem Ordering.isLT_iff_eq_lt {o : Ordering} :

o.isLT = true ↔ o = lt

source

theorem Ordering.isLE_iff_eq_lt_or_eq_eq {o : Ordering} :

o.isLE = true ↔ o = lt ∨ o = eq

source

theorem Ordering.isLE_of_eq_lt {o : Ordering} :

o = lt → o.isLE = true

source

theorem Ordering.isLE_of_eq_eq {o : Ordering} :

o = eq → o.isLE = true

source

theorem Ordering.isEq_iff_eq_eq {o : Ordering} :

o.isEq = true ↔ o = eq

source

theorem Ordering.isNe_iff_ne_eq {o : Ordering} :

o.isNe = true ↔ o ≠ eq

source

theorem Ordering.isGE_iff_eq_gt_or_eq_eq {o : Ordering} :

o.isGE = true ↔ o = gt ∨ o = eq

source

theorem Ordering.isGE_of_eq_gt {o : Ordering} :

o = gt → o.isGE = true

source

theorem Ordering.isGE_of_eq_eq {o : Ordering} :

o = eq → o.isGE = true

source

theorem Ordering.isGT_iff_eq_gt {o : Ordering} :

o.isGT = true ↔ o = gt

source

@[simp]

theorem Ordering.swap_swap {o : Ordering} :

o.swap.swap = o

source

@[simp]

theorem Ordering.swap_inj {o₁ o₂ : Ordering} :

o₁.swap = o₂.swap ↔ o₁ = o₂

source

theorem Ordering.swap_then (o₁ o₂ : Ordering) :

(o₁.then o₂).swap = o₁.swap.then o₂.swap

source

theorem Ordering.then_eq_lt {o₁ o₂ : Ordering} :

o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt

source

theorem Ordering.then_eq_eq {o₁ o₂ : Ordering} :

o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq

source

theorem Ordering.then_eq_gt {o₁ o₂ : Ordering} :

o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt

source

@[inline]

def compareOfLessAndEq {α : Type u_1} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] :

Ordering

Yields an Ordering s.t. x < y corresponds to Ordering.lt / Ordering.gt and x = y corresponds to Ordering.eq.

Equations

compareOfLessAndEq x y = if x < y then Ordering.lt else if x = y then Ordering.eq else Ordering.gt

source

@[inline]

def compareOfLessAndBEq {α : Type u_1} (x y : α) [LT α] [Decidable (x < y)] [BEq α] :

Ordering

Yields an Ordering s.t. x < y corresponds to Ordering.lt / Ordering.gt and x == y corresponds to Ordering.eq.

Equations

compareOfLessAndBEq x y = if x < y then Ordering.lt else if (x == y) = true then Ordering.eq else Ordering.gt

source

@[inline]

def compareLex {α : Sort u_1} {β : Sort u_2} (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) :

Ordering

Compare a and b lexicographically by cmp₁ and cmp₂. a and b are first compared by cmp₁. If this returns 'equal', a and b are compared by cmp₂ to break the tie.

Equations