Documentation

Init.Data.Ord

inductive Ordering:

Type

instance instInhabitedOrdering:

Inhabited Ordering

Equations

instInhabitedOrdering = { default := Ordering.lt }

instance instBEqOrdering:

Equations

instBEqOrdering = { beq := [anonymous] }

class Ord (α : Type u) :

Type u

compare : α → α → Ordering

Instances

@[inline]

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

Equations

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

instance instOrdNat:

Equations

instOrdNat = { compare := fun x y => compareOfLessAndEq x y }

instance instOrdInt:

Equations

instOrdInt = { compare := fun x y => compareOfLessAndEq x y }

instance instOrdBool:

Equations

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

instance instOrdString:

Equations

instOrdString = { compare := fun x y => compareOfLessAndEq x y }

instance instOrdFin (n : Nat) :

Equations

instOrdFin n = { compare := fun x y => compare x.val y.val }

instance instOrdUInt8:

Equations

instOrdUInt8 = { compare := fun x y => compareOfLessAndEq x y }

instance instOrdUInt16:

Equations

instOrdUInt16 = { compare := fun x y => compareOfLessAndEq x y }

instance instOrdUInt32:

Equations

instOrdUInt32 = { compare := fun x y => compareOfLessAndEq x y }

instance instOrdUInt64:

Equations

instOrdUInt64 = { compare := fun x y => compareOfLessAndEq x y }

instance instOrdUSize:

Equations

instOrdUSize = { compare := fun x y => compareOfLessAndEq x y }

instance instOrdChar:

Equations

instOrdChar = { compare := fun x y => compareOfLessAndEq x y }

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

LT α

Equations

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

instance instDecidableRelLtLtOfOrd {α : Type u_1} [inst : 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 _fun_discr = match _fun_discr with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

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

LE α

Equations

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

instance instDecidableRelLeLeOfOrd {α : Type u_1} [inst : Ord α] :

DecidableRel LE.le

Equations

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