← Copula mathematical handbook

Instances for fixed width signed integer types.

@[instance_reducible]

instance Int8.instOrd : Ord Int8

Equations

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

instance Int8.instTransOrd : Std.TransOrd Int8

instance Int8.instLawfulEqOrd : Std.LawfulEqOrd Int8

instance Int8.instLawfulOrderOrd : Std.LawfulOrderOrd Int8

@[instance_reducible]

instance Int16.instOrd : Ord Int16

Equations

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

instance Int16.instTransOrd : Std.TransOrd Int16

instance Int16.instLawfulEqOrd : Std.LawfulEqOrd Int16

instance Int16.instLawfulOrderOrd : Std.LawfulOrderOrd Int16

@[instance_reducible]

instance Int32.instOrd : Ord Int32

Equations

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

instance Int32.instTransOrd : Std.TransOrd Int32

instance Int32.instLawfulEqOrd : Std.LawfulEqOrd Int32

instance Int32.instLawfulOrderOrd : Std.LawfulOrderOrd Int32

@[instance_reducible]

instance Int64.instOrd : Ord Int64

Equations

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

instance Int64.instTransOrd : Std.TransOrd Int64

instance Int64.instLawfulEqOrd : Std.LawfulEqOrd Int64

instance Int64.instLawfulOrderOrd : Std.LawfulOrderOrd Int64

@[instance_reducible]

instance ISize.instOrd : Ord ISize

Equations

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

instance ISize.instTransOrd : Std.TransOrd ISize

instance ISize.instLawfulEqOrd : Std.LawfulEqOrd ISize

instance ISize.instLawfulOrderOrd : Std.LawfulOrderOrd ISize