Equations
- instInhabitedOrdering = { default := Ordering.lt }
- compare : α → α → Ordering
@[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
Equations
- instOrdNat = { compare := fun x y => compareOfLessAndEq x y }
Equations
- instOrdInt = { compare := fun x y => compareOfLessAndEq x y }
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 }
Equations
- instOrdString = { compare := fun x y => compareOfLessAndEq x y }
Equations
- instOrdFin n = { compare := fun x y => compare x.val y.val }
Equations
- instOrdUInt8 = { compare := fun x y => compareOfLessAndEq x y }
Equations
- instOrdUInt16 = { compare := fun x y => compareOfLessAndEq x y }
Equations
- instOrdUInt32 = { compare := fun x y => compareOfLessAndEq x y }
Equations
- instOrdUInt64 = { compare := fun x y => compareOfLessAndEq x y }
Equations
- instOrdUSize = { compare := fun x y => compareOfLessAndEq x y }
Equations
- instOrdChar = { compare := fun x y => compareOfLessAndEq x y }
Equations
- instDecidableRelLtLtOfOrd = inferInstanceAs (DecidableRel fun a b => (compare a b == Ordering.lt) = true)
Equations
- Ordering.isLE x = match x with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false
Equations
- instDecidableRelLeLeOfOrd = inferInstanceAs (DecidableRel fun a b => Ordering.isLE (compare a b) = true)