# Documentation

## Init.Data.Ord

inductive Ordering :
Instances For
Equations
• = if h : then else

Swaps less and greater ordering results

Equations
Instances For
@[macro_inline]

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
Instances For

Check whether the ordering is 'equal'.

Equations
• = match x with | Ordering.eq => true | x => false
Instances For

Check whether the ordering is 'not equal'.

Equations
• = match x with | Ordering.eq => false | x => true
Instances For

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

Equations
• = match x with | Ordering.gt => false | x => true
Instances For

Check whether the ordering is 'less than'.

Equations
• = match x with | Ordering.lt => true | x => false
Instances For

Check whether the ordering is 'greater than'.

Equations
• = match x with | Ordering.gt => true | x => false
Instances For

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

Equations
• = match x with | Ordering.lt => false | x => true
Instances For
@[inline]
def compareOfLessAndEq {α : Type u_1} (x : α) (y : α) [LT α] [Decidable (x < y)] [] :
Equations
Instances For
@[inline]
def compareLex {α : Sort u_1} {β : Sort u_2} (cmp₁ : αβOrdering) (cmp₂ : αβOrdering) (a : α) (b : β) :

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
Instances For
class Ord (α : Type u) :
Instances
@[inline]
def compareOn {β : Type u_1} {α : Sort u_2} [ord : Ord β] (f : αβ) (x : α) (y : α) :

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

Equations
Instances For
instance instOrdNat :
Equations
instance instOrdInt :
Equations
instance instOrdBool :
Equations
instance instOrdString :
Equations
instance instOrdFin (n : Nat) :
Ord (Fin n)
Equations
• = { compare := fun (x y : Fin n) => compare x y }
instance instOrdUInt8 :
Equations
instance instOrdUInt16 :
Equations
instance instOrdUInt32 :
Equations
instance instOrdUInt64 :
Equations
instance instOrdUSize :
Equations
instance instOrdChar :
Equations
def lexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
Ord (α × β)

The lexicographic order on pairs.

Equations
• lexOrd = { compare := fun (p1 p2 : α × β) => match compare p1.fst p2.fst with | Ordering.eq => compare p1.snd p2.snd | o => o }
Instances For
def ltOfOrd {α : Type u_1} [Ord α] :
LT α
Equations
• ltOfOrd = { lt := fun (a b : α) => () = true }
Instances For
instance instDecidableRelLtLtOfOrd {α : Type u_1} [Ord α] :
Equations
def leOfOrd {α : Type u_1} [Ord α] :
LE α
Equations
Instances For
instance instDecidableRelLeLeOfOrd {α : Type u_1} [Ord α] :
Equations
def Ord.toBEq {α : Type u_1} (ord : Ord α) :
BEq α

Derive a BEq instance from an Ord instance.

Equations
Instances For
def Ord.toLT {α : Type u_1} :
Ord αLT α

Derive an LT instance from an Ord instance.

Equations
• = ltOfOrd
Instances For
def Ord.toLE {α : Type u_1} :
Ord αLE α

Derive an LE instance from an Ord instance.

Equations
• = leOfOrd
Instances For
def Ord.opposite {α : Type u_1} (ord : Ord α) :
Ord α

Invert the order of an Ord instance.

Equations
Instances For
def Ord.on {β : Type u_1} {α : Type u_2} (ord : Ord β) (f : αβ) :
Ord α

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

Equations
Instances For
def Ord.lex {α : Type u_1} {β : Type u_2} :
Ord αOrd βOrd (α × β)

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

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

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

Equations
Instances For