Init.Data.Ord

If a and b are Ordering, then a.then b returns a unless it is .eq, in which case it returns b. Additionally, it has “short-circuiting” behavior similar to boolean &&: if a is not .eq then the expression for b is not evaluated.

This is a useful primitive for constructing lexicographic comparator functions. The deriving Ord syntax on a structure uses the Ord instance to compare each field in order, combining the results equivalently to Ordering.then.

Use compareLex to lexicographically combine two comparison functions.

Examples:

structure Person where
  name : String
  age : Nat

-- Sort people first by name (in ascending order), and people with the same name by age (in
-- descending order)
instance : Ord Person where
  compare a b := (compare a.name b.name).then (compare b.age a.age)

#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Dana", 50⟩

Ordering.gt

#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 50⟩

Ordering.gt

#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 20⟩

Ordering.lt

Equations

Ordering.eq.then b = b
a.then b = a

source

def Ordering.isEq :

Ordering → Bool

Checks whether the ordering is eq.

Equations

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

source

def Ordering.isNe :

Ordering → Bool

Checks whether the ordering is not eq.

Equations

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

source

def Ordering.isLE :

Ordering → Bool

Checks whether the ordering is lt or eq.

Equations

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

source

def Ordering.isLT :

Ordering → Bool

Checks whether the ordering is lt.

Equations

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

source

def Ordering.isGT :

Ordering → Bool

Checks whether the ordering is gt.

Equations

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

source

def Ordering.isGE :

Ordering → Bool

Checks whether the ordering is gt or eq.

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

@[simp]

theorem Ordering.lt_then {o : Ordering} :

lt.then o = lt

source

@[simp]

theorem Ordering.gt_then {o : Ordering} :

gt.then o = gt

source

@[simp]

theorem Ordering.eq_then {o : Ordering} :

eq.then o = o

source

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

(o₁.then o₂).isLE = true ↔ o₁ = lt ∨ o₁ = eq ∧ o₂.isLE = true

source

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

(o₁.then o₂).isLE = true ↔ o₁.isLE = true ∧ (o₁ = lt ∨ o₂.isLE = true)

source

theorem Ordering.isLE_left_of_isLE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isLE = true) :

o₁.isLE = true

source

theorem Ordering.isGE_left_of_isGE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isGE = true) :

o₁.isGE = true

source

@[inline]

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

Ordering

Uses decidable less-than and equality relations to find an Ordering.

In particular, if x < y then the result is Ordering.lt. If x = y then the result is Ordering.eq. Otherwise, it is Ordering.gt.

compareOfLessAndBEq uses BEq instead of DecidableEq.

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

Uses a decidable less-than relation and Boolean equality to find an Ordering.

In particular, if x < y then the result is Ordering.lt. If x == y then the result is Ordering.eq. Otherwise, it is Ordering.gt.

compareOfLessAndEq uses DecidableEq instead of BEq.

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

Compares a and b lexicographically by cmp₁ and cmp₂.

a and b are first compared by cmp₁. If this returns Ordering.eq, a and b are compared by cmp₂ to break the tie.

To lexicographically combine two Orderings, use Ordering.then.

Equations

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

Instances For

source

@[simp]

theorem compareLex_eq_eq {α : Sort u_1} {cmp₁ cmp₂ : α → α → Ordering} {a b : α} :

compareLex cmp₁ cmp₂ a b = Ordering.eq ↔ cmp₁ a b = Ordering.eq ∧ cmp₂ a b = Ordering.eq

source

theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α] [DecidableLT α] [DecidableEq α] (h : ∀ (x y : α), x < y ↔ ¬y < x ∧ x ≠ y) {x y : α} :

compareOfLessAndEq x y = (compareOfLessAndEq y x).swap

source

theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) (x y : α) :

x < y ↔ ¬y < x ∧ x ≠ y

source

theorem compareOfLessAndEq_eq_swap {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) {x y : α} :

compareOfLessAndEq x y = (compareOfLessAndEq y x).swap

source

@[simp]

theorem compareOfLessAndEq_eq_lt {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α} :

compareOfLessAndEq x y = Ordering.lt ↔ x < y

source

theorem compareOfLessAndEq_eq_eq {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α] (refl : ∀ (x : α), x ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) {x y : α} :

compareOfLessAndEq x y = Ordering.eq ↔ x = y

source

theorem compareOfLessAndEq_eq_gt_of_lt_iff_not_gt_and_ne {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α} (h : ∀ (x y : α), x < y ↔ ¬y < x ∧ x ≠ y) :

compareOfLessAndEq x y = Ordering.gt ↔ y < x

source

theorem compareOfLessAndEq_eq_gt {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) (x y : α) :

compareOfLessAndEq x y = Ordering.gt ↔ y < x

source

theorem isLE_compareOfLessAndEq {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) {x y : α} :

(compareOfLessAndEq x y).isLE = true ↔ x ≤ y

source

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.

Instances

source

@[inline]

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

Ordering

Compares two values by comparing the results of applying a function.

In particular, x is compared to y by comparing f x and f y.

Examples:

compareOn (·.length) "apple" "banana" = .lt
compareOn (· % 3) 5 6 = .gt
compareOn (·.foldl max 0) [1, 2, 3] [3, 2, 1] = .eq

Equations

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

Instances For

source

instance instOrdNat :

Ord Nat

Equations

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

source

instance instOrdInt :

Ord Int

Equations

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

source

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 }

source

instance instOrdString :

Ord String

Equations

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

source

instance instOrdFin (n : Nat) :

Ord (Fin n)

Equations

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

source

instance instOrdUInt8 :

Ord UInt8

Equations

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

source

instance instOrdUInt16 :

Ord UInt16

Equations

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

source

instance instOrdUInt32 :

Ord UInt32

Equations

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

source

instance instOrdUInt64 :

Ord UInt64

Equations

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

source

instance instOrdUSize :

Ord USize

Equations

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

source

instance instOrdChar :

Ord Char

Equations

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

source

instance instOrdInt8 :

Ord Int8

Equations

instOrdInt8 = { compare := fun (x y : Int8) => compareOfLessAndEq x y }

source

instance instOrdInt16 :

Ord Int16

Equations

instOrdInt16 = { compare := fun (x y : Int16) => compareOfLessAndEq x y }

source

instance instOrdInt32 :

Ord Int32

Equations

instOrdInt32 = { compare := fun (x y : Int32) => compareOfLessAndEq x y }

source

instance instOrdInt64 :

Ord Int64

Equations

instOrdInt64 = { compare := fun (x y : Int64) => compareOfLessAndEq x y }

source

instance instOrdISize :

Ord ISize

Equations

instOrdISize = { compare := fun (x y : ISize) => compareOfLessAndEq x y }

source

instance instOrdBitVec {n : Nat} :

Ord (BitVec n)

Equations

instOrdBitVec = { compare := fun (x y : BitVec n) => compareOfLessAndEq x y }

source

instance instOrdOption {α : Type u_1} [Ord α] :

Ord (Option α)

Equations

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

source

instance instOrdOrdering :

Ord Ordering

Equations

instOrdOrdering = { compare := compareOn fun (x : Ordering) => x.toCtorIdx }

source

@[specialize #[]]

def List.compareLex {α : Type u_1} (cmp : α → α → Ordering) :

List α → List α → Ordering

Equations

List.compareLex cmp [] [] = Ordering.eq
List.compareLex cmp [] x✝ = Ordering.lt
List.compareLex cmp x✝ [] = Ordering.gt
List.compareLex cmp (x_2 :: xs) (y :: ys) = match cmp x_2 y with | Ordering.lt => Ordering.lt | Ordering.eq => List.compareLex cmp xs ys | Ordering.gt => Ordering.gt

Instances For

source

instance List.instOrd {α : Type u_1} [Ord α] :

Ord (List α)

Equations

List.instOrd = { compare := List.compareLex compare }

source

theorem List.compare_eq_compareLex {α : Type u_1} [Ord α] :

compare = List.compareLex compare

source

theorem List.compareLex_cons_cons {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {xs ys : List α} :

List.compareLex cmp (x :: xs) (y :: ys) = (cmp x y).then (List.compareLex cmp xs ys)

source

@[simp]

theorem List.compare_cons_cons {α : Type u_1} [Ord α] {x y : α} {xs ys : List α} :

compare (x :: xs) (y :: ys) = (compare x y).then (compare xs ys)

source

theorem List.compareLex_nil_cons {α : Type u_1} {cmp : α → α → Ordering} {x : α} {xs : List α} :

List.compareLex cmp [] (x :: xs) = Ordering.lt

source

@[simp]

theorem List.compare_nil_cons {α : Type u_1} [Ord α] {x : α} {xs : List α} :

compare [] (x :: xs) = Ordering.lt

source

theorem List.compareLex_cons_nil {α : Type u_1} {cmp : α → α → Ordering} {x : α} {xs : List α} :

List.compareLex cmp (x :: xs) [] = Ordering.gt

source

@[simp]

theorem List.compare_cons_nil {α : Type u_1} [Ord α] {x : α} {xs : List α} :

compare (x :: xs) [] = Ordering.gt

source

theorem List.compareLex_nil_nil {α : Type u_1} {cmp : α → α → Ordering} :

List.compareLex cmp [] [] = Ordering.eq

source

@[simp]

theorem List.compare_nil_nil {α : Type u_1} [Ord α] :

compare [] [] = Ordering.eq

source

theorem List.isLE_compareLex_nil_left {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} :

(List.compareLex cmp [] xs).isLE = true

source

theorem List.isLE_compare_nil_left {α : Type u_1} [Ord α] {xs : List α} :

(compare [] xs).isLE = true

source

theorem List.isLE_compareLex_nil_right {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} :

(List.compareLex cmp xs []).isLE = true ↔ xs = []

source

@[simp]

theorem List.isLE_compare_nil_right {α : Type u_1} [Ord α] {xs : List α} :

(compare xs []).isLE = true ↔ xs = []

source

theorem List.isGE_compareLex_nil_left {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} :

(List.compareLex cmp [] xs).isGE = true ↔ xs = []

source

@[simp]

theorem List.isGE_compare_nil_left {α : Type u_1} [Ord α] {xs : List α} :

(compare [] xs).isGE = true ↔ xs = []

source

theorem List.isGE_compareLex_nil_right {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} :

(List.compareLex cmp xs []).isGE = true

source

theorem List.isGE_compare_nil_right {α : Type u_1} [Ord α] {xs : List α} :

(compare xs []).isGE = true

source

theorem List.compareLex_nil_left_eq_eq {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} :

List.compareLex cmp [] xs = Ordering.eq ↔ xs = []

source

@[simp]

theorem List.compare_nil_left_eq_eq {α : Type u_1} [Ord α] {xs : List α} :

compare [] xs = Ordering.eq ↔ xs = []

source

theorem List.compareLex_nil_right_eq_eq {α : Type u_1} {cmp : α → α → Ordering} {xs : List α} :

List.compareLex cmp xs [] = Ordering.eq ↔ xs = []

source

@[simp]

theorem List.compare_nil_right_eq_eq {α : Type u_1} [Ord α] {xs : List α} :

compare xs [] = Ordering.eq ↔ xs = []

source

@[specialize #[]]

def Array.compareLex {α : Type u_1} (cmp : α → α → Ordering) (a₁ a₂ : Array α) :

Ordering

Equations

Array.compareLex cmp a₁ a₂ = Array.compareLex.go cmp a₁ a₂ 0

Instances For

source

@[irreducible]

def Array.compareLex.go {α : Type u_1} (cmp : α → α → Ordering) (a₁ a₂ : Array α) (i : Nat) :

Ordering

Equations

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

source

instance Array.instOrd {α : Type u_1} [Ord α] :

Ord (Array α)

Equations

Array.instOrd = { compare := Array.compareLex compare }

source

theorem Array.compare_eq_compareLex {α : Type u_1} [Ord α] :

compare = Array.compareLex compare

source

theorem List.compareLex_eq_compareLex_toArray {α : Type u_1} {cmp : α → α → Ordering} {l₁ l₂ : List α} :

List.compareLex cmp l₁ l₂ = Array.compareLex cmp l₁.toArray l₂.toArray

source

theorem List.compare_eq_compare_toArray {α : Type u_1} [Ord α] {l₁ l₂ : List α} :

compare l₁ l₂ = compare l₁.toArray l₂.toArray

source

theorem Array.compareLex_eq_compareLex_toList {α : Type u_1} {cmp : α → α → Ordering} {a₁ a₂ : Array α} :

Array.compareLex cmp a₁ a₂ = List.compareLex cmp a₁.toList a₂.toList

source

theorem Array.compare_eq_compare_toList {α : Type u_1} [Ord α] {a₁ a₂ : Array α} :

compare a₁ a₂ = compare a₁.toList a₂.toList

source

def Vector.compareLex {α : Type u_1} {n : Nat} (cmp : α → α → Ordering) (a b : Vector α n) :

Ordering

Equations

Vector.compareLex cmp a b = Array.compareLex cmp a.toArray b.toArray

Instances For

source

instance Vector.instOrd {α : Type u_1} {n : Nat} [Ord α] :

Ord (Vector α n)

Equations

Vector.instOrd = { compare := Vector.compareLex compare }

source

theorem Vector.compareLex_eq_compareLex_toArray {α : Type u_1} {n : Nat} {cmp : α → α → Ordering} {a b : Vector α n} :

Vector.compareLex cmp a b = Array.compareLex cmp a.toArray b.toArray

source

theorem Vector.compareLex_eq_compareLex_toList {α : Type u_1} {n : Nat} {cmp : α → α → Ordering} {a b : Vector α n} :

Vector.compareLex cmp a b = List.compareLex cmp a.toList b.toList

source

theorem Vector.compare_eq_compare_toArray {α : Type u_1} {n : Nat} [Ord α] {a b : Vector α n} :

compare a b = compare a.toArray b.toArray

source

theorem Vector.compare_eq_compare_toList {α : Type u_1} {n : Nat} [Ord α] {a b : Vector α n} :

compare a b = compare a.toList b.toList

source

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) }

source

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

LT α

Constructs an LT instance from an Ord instance that asserts that the result of compare is Ordering.lt.

Equations

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

source

instance instDecidableRelLt {α : Type u_1} [Ord α] :

DecidableRel LT.lt

Equations

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

source

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

LE α

Constructs an LT instance from an Ord instance that asserts that the result of compare satisfies Ordering.isLE.

Equations

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

source

instance instDecidableRelLe {α : Type u_1} [Ord α] :

DecidableRel LE.le

Equations

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

source

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

BEq α

Constructs a BEq instance from an Ord instance.

Equations

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

source

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

LT α

Constructs an LT instance from an Ord instance.

Equations

ord.toLT = ltOfOrd

source

instance Ord.instDecidableRelLt {α : Type u_1} [i : Ord α] :

DecidableRel LT.lt

Equations

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

source

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

LE α

Constructs an LE instance from an Ord instance.

Equations

ord.toLE = leOfOrd

source

instance Ord.instDecidableRelLe {α : Type u_1} [i : Ord α] :

DecidableRel LE.le

Equations

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

source

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

Ord α

Inverts the order of an Ord instance.

The result is an Ord α instance that returns Ordering.lt when ord would return Ordering.gt and that returns Ordering.gt when ord would return Ordering.lt.

Equations

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

source

def Ord.on {β : Type u_1} {α : Type u_2} :

Ord β → (f : α → β) → Ord α

Constructs an Ord instance that compares values according to the results of f.

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

The function compareOn can be used to perform this comparison without constructing an intermediate Ord instance.

Equations

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

source

def Ord.lex {α : Type u_1} {β : Type u_2} :

Ord α → Ord β → Ord (α × β)

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

Equations

x✝¹.lex x✝ = lexOrd

source

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

Ord α

Constructs an Ord instance from two existing instances by combining them lexicographically.

The resulting instance compares elements first by ord₁ and then, if this returns Ordering.eq, by ord₂.

The function compareLex can be used to perform this comparison without constructing an intermediate Ord instance. Ordering.then can be used to lexicographically combine the results of comparisons.

Equations

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

source

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

Ord (Array α)

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

Equations

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