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

class Ord (α : Type u) : Type u

• compare : α → α → Ordering

@[inline]

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

Equations

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

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.val y.val }

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 }

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 }

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

Equations

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

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

Equations

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

def Ordering.isLE : Ordering → Bool

Equations

• Ordering.isLE x = match x with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

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

Equations

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

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

Equations

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