Documentation

Init.Data.Ord

inductive Ordering :

Type

lt: Ordering
eq: Ordering
gt: Ordering

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 _fun_discr _fun_discr_1 => match _fun_discr, _fun_discr_1 with | false, true => Ordering.lt | true, false => Ordering.gt | x, x_1 => 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)