← Copula mathematical handbook

Instances for fixed width unsigned integer types.

@[instance_reducible]

instance UInt8.instOrd : Ord UInt8

Equations

• UInt8.instOrd = { compare := fun (x y : UInt8) => compareOfLessAndEq x y }

instance UInt8.instTransOrd : Std.TransOrd UInt8

instance UInt8.instLawfulEqOrd : Std.LawfulEqOrd UInt8

instance UInt8.instLawfulOrderOrd : Std.LawfulOrderOrd UInt8

@[instance_reducible]

instance UInt16.instOrd : Ord UInt16

Equations

• UInt16.instOrd = { compare := fun (x y : UInt16) => compareOfLessAndEq x y }

instance UInt16.instTransOrd : Std.TransOrd UInt16

instance UInt16.instLawfulEqOrd : Std.LawfulEqOrd UInt16

instance UInt16.instLawfulOrderOrd : Std.LawfulOrderOrd UInt16

@[instance_reducible]

instance UInt32.instOrd : Ord UInt32

Equations

• UInt32.instOrd = { compare := fun (x y : UInt32) => compareOfLessAndEq x y }

instance UInt32.instTransOrd : Std.TransOrd UInt32

instance UInt32.instLawfulEqOrd : Std.LawfulEqOrd UInt32

instance UInt32.instLawfulOrderOrd : Std.LawfulOrderOrd UInt32

@[instance_reducible]

instance UInt64.instOrd : Ord UInt64

Equations

• UInt64.instOrd = { compare := fun (x y : UInt64) => compareOfLessAndEq x y }

instance UInt64.instTransOrd : Std.TransOrd UInt64

instance UInt64.instLawfulEqOrd : Std.LawfulEqOrd UInt64

instance UInt64.instLawfulOrderOrd : Std.LawfulOrderOrd UInt64

@[instance_reducible]

instance USize.instOrd : Ord USize

Equations

• USize.instOrd = { compare := fun (x y : USize) => compareOfLessAndEq x y }

instance USize.instTransOrd : Std.TransOrd USize

instance USize.instLawfulEqOrd : Std.LawfulEqOrd USize

instance USize.instLawfulOrderOrd : Std.LawfulOrderOrd USize