ink

instance Ordering.instDecidableEqOrdering : DecidableEq Ordering

Equations

• Ordering.instDecidableEqOrdering x y = if h : Ordering.toCtorIdx x = Ordering.toCtorIdx y then isTrue (_ : x = y) else isFalse (_ : x = y → False)

ink

def Ordering.swap : Ordering → Ordering

Swaps less and greater ordering results

Equations

• Ordering.swap x = match x with | Ordering.lt => Ordering.gt | Ordering.eq => Ordering.eq | Ordering.gt => Ordering.lt

ink

@[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.then x x = match x, x with | Ordering.eq, f => f | o, x => o

ink

def Ordering.isEq : Ordering → Bool

Check whether the ordering is 'equal'.

Equations

• Ordering.isEq x = match x with | Ordering.eq => true | x => false

ink

def Ordering.isNe : Ordering → Bool

Check whether the ordering is 'not equal'.

Equations

• Ordering.isNe x = match x with | Ordering.eq => false | x => true

ink

def Ordering.isLT : Ordering → Bool

Check whether the ordering is 'less than'.

Equations

• Ordering.isLT x = match x with | Ordering.lt => true | x => false

ink

def Ordering.isGT : Ordering → Bool

Check whether the ordering is 'greater than'.

Equations

• Ordering.isGT x = match x with | Ordering.gt => true | x => false

ink

def Ordering.isGE : Ordering → Bool

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

Equations

• Ordering.isGE x = match x with | Ordering.lt => false | x => true

ink

@[inline]

def compareLex {α : Sort u_1} {β : Sort u_2} (cmp₁ : α → β → Ordering) (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 = Ordering.then (cmp₁ a b) (cmp₂ a b)

ink

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

ink

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

Derive a BEq instance from an Ord instance.

Equations

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

ink

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

Derive an LT instance from an Ord instance.

Equations

• Ord.toLT x = ltOfOrd

ink

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

Derive an LE instance from an Ord instance.

Equations

• Ord.toLE x = leOfOrd

ink

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

Invert the order of an Ord instance.

Equations

• Ord.opposite ord = { compare := fun x y => compare y x }

ink

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

• Ord.on ord f = { compare := compareOn f }

ink

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

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

Equations

• Ord.lex x x = lexOrd

ink

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

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