@[instance_reducible]

instance instOrdUnit_dY : Ord Unit

Equations

• instOrdUnit_dY = { compare := fun (x x_1 : Unit) => Ordering.eq }

instance instReflOrdUnit_dY : Std.ReflOrd Unit

instance instLawfulEqOrdUnit_dY : Std.LawfulEqOrd Unit

instance instOrientedOrdUnit_dY : Std.OrientedOrd Unit

instance instTransOrdUnit_dY : Std.TransOrd Unit

def ByteArray.compare (x y : ByteArray) : Ordering

Equations

• x.compare y = compare x.data y.data

@[instance_reducible]

instance instOrdByteArray_dY : Ord ByteArray

Equations

• instOrdByteArray_dY = { compare := fun (x y : ByteArray) => x.compare y }

instance instReflOrdByteArray_dY : Std.ReflOrd ByteArray

instance instLawfulEqOrdByteArray_dY : Std.LawfulEqOrd ByteArray

instance instOrientedOrdByteArray_dY : Std.OrientedOrd ByteArray

instance instTransOrdByteArray_dY : Std.TransOrd ByteArray