inductive Ordering : Type

• lt : Ordering
• eq : Ordering
• gt : Ordering

instance instInhabitedOrdering : Inhabited Ordering

Equations

• instInhabitedOrdering = { default := Ordering.lt }

instance instBEqOrdering : BEq Ordering

Equations

• instBEqOrdering = { beq := beqOrdering✝ }

instance Ordering.instDecidableEq : DecidableEq Ordering

Equations

• x✝.instDecidableEq y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

def Ordering.swap : Ordering → Ordering

Swaps less and greater ordering results

Equations

• Ordering.lt.swap = Ordering.gt
• Ordering.eq.swap = Ordering.eq
• Ordering.gt.swap = Ordering.lt

@[macro_inline]

def Ordering.then : Ordering → Ordering → Ordering

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 x✝ = x✝
• x✝¹.then x✝ = x✝¹

def Ordering.isEq : Ordering → Bool

Check whether the ordering is 'equal'.

Equations

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

def Ordering.isNe : Ordering → Bool

Check whether the ordering is 'not equal'.

Equations

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

def Ordering.isLE : Ordering → Bool

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

Equations

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

def Ordering.isLT : Ordering → Bool

Check whether the ordering is 'less than'.

Equations

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

def Ordering.isGT : Ordering → Bool

Check whether the ordering is 'greater than'.

Equations

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

def Ordering.isGE : Ordering → Bool

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

Equations

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

@[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

@[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

@[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

• compareLex cmp₁ cmp₂ a b = (cmp₁ a b).then (cmp₂ a b)

class Ord (α : Type u) : Type u

Ord α provides a computable total order on α, in terms of the compare : α → α → Ordering function.

Typically instances will be transitive, reflexive, and antisymmetric, but this is not enforced by the typeclass.

There is a derive handler, so appending deriving Ord to an inductive type or structure will attempt to create an Ord instance.

• compare : α → α → Ordering

  Compare two elements in α using the comparator contained in an [Ord α] instance.

@[inline]

def compareOn {β : Type u_1} {α : Sort u_2} [ord : Ord β] (f : α → β) (x y : α) : Ordering

Compare x and y by comparing f x and f y.

Equations

• compareOn f x y = compare (f x) (f y)

instance instOrdNat : Ord Nat

Equations

• instOrdNat = { compare := fun (x y : Nat) => compareOfLessAndEq x y }

instance instOrdInt : Ord Int

Equations

• instOrdInt = { compare := fun (x y : Int) => compareOfLessAndEq x y }

instance instOrdBool : Ord Bool

Equations

• instOrdBool = { compare := fun (x x_1 : Bool) => match x, x_1 with | false, true => Ordering.lt | true, false => Ordering.gt | x, x_2 => Ordering.eq }

instance instOrdString : Ord String

Equations

• instOrdString = { compare := fun (x y : String) => compareOfLessAndEq x y }

instance instOrdFin (n : Nat) : Ord (Fin n)

Equations

• instOrdFin n = { compare := fun (x y : Fin n) => compare ↑x ↑y }

instance instOrdUInt8 : Ord UInt8

Equations

• instOrdUInt8 = { compare := fun (x y : UInt8) => compareOfLessAndEq x y }

instance instOrdUInt16 : Ord UInt16

Equations

• instOrdUInt16 = { compare := fun (x y : UInt16) => compareOfLessAndEq x y }

instance instOrdUInt32 : Ord UInt32

Equations

• instOrdUInt32 = { compare := fun (x y : UInt32) => compareOfLessAndEq x y }

instance instOrdUInt64 : Ord UInt64

Equations

• instOrdUInt64 = { compare := fun (x y : UInt64) => compareOfLessAndEq x y }

instance instOrdUSize : Ord USize

Equations

• instOrdUSize = { compare := fun (x y : USize) => compareOfLessAndEq x y }

instance instOrdChar : Ord Char

Equations

• instOrdChar = { compare := fun (x y : Char) => compareOfLessAndEq x y }

instance instOrdOption {α : Type u_1} [Ord α] : Ord (Option α)

Equations

• One or more equations did not get rendered due to their size.

def lexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] : Ord (α × β)

The lexicographic order on pairs.

Equations

• lexOrd = { compare := compareLex (compareOn fun (x : α × β) => x.fst) (compareOn fun (x : α × β) => x.snd) }

def ltOfOrd {α : Type u_1} [Ord α] : LT α

Equations

• ltOfOrd = { lt := fun (a b : α) => compare a b = Ordering.lt }

instance instDecidableRelLt {α : Type u_1} [Ord α] : DecidableRel LT.lt

Equations

• instDecidableRelLt = inferInstanceAs (DecidableRel fun (a b : α) => compare a b = Ordering.lt)

def leOfOrd {α : Type u_1} [Ord α] : LE α

Equations

• leOfOrd = { le := fun (a b : α) => (compare a b).isLE = true }

instance instDecidableRelLe {α : Type u_1} [Ord α] : DecidableRel LE.le

Equations

• instDecidableRelLe = inferInstanceAs (DecidableRel fun (a b : α) => (compare a b).isLE = true)

def Ord.toBEq {α : Type u_1} (ord : Ord α) : BEq α

Derive a BEq instance from an Ord instance.

Equations

• ord.toBEq = { beq := fun (x y : α) => compare x y == Ordering.eq }

def Ord.toLT {α : Type u_1} : Ord α → LT α

Derive an LT instance from an Ord instance.

Equations

• x✝.toLT = ltOfOrd

def Ord.toLE {α : Type u_1} : Ord α → LE α

Derive an LE instance from an Ord instance.

Equations

• x✝.toLE = leOfOrd

def Ord.opposite {α : Type u_1} (ord : Ord α) : Ord α

Invert the order of an Ord instance.

Equations

• ord.opposite = { compare := fun (x y : α) => compare y x }

def Ord.on {β : Type u_1} {α : Type u_2} : Ord β → (f : α → β) → Ord α

ord.on f compares x and y by comparing f x and f y according to ord.

Equations

• x✝.on f = { compare := compareOn f }

def Ord.lex {α : Type u_1} {β : Type u_2} : Ord α → Ord β → Ord (α × β)

Derive the lexicographic order on products α × β from orders for α and β.

Equations

• x✝¹.lex x✝ = lexOrd

def Ord.lex' {α : Type u_1} (ord₁ ord₂ : Ord α) : Ord α

Create an order which compares elements first by ord₁ and then, if this returns 'equal', by ord₂.

Equations

• ord₁.lex' ord₂ = { compare := compareLex compare compare }

def Ord.arrayOrd {α : Type u_1} [a : Ord α] : Ord (Array α)

Creates an order which compares elements of an Array in lexicographic order.

Equations

• Ord.arrayOrd = { compare := fun (x y : Array α) => let x_1 := a.toLT; let x_2 := a.toBEq; compareOfLessAndBEq x.toList y.toList }