Make.E
The function compare
decides a relation \leq
over elements of type t
.
The relation \leq
must be a total preorder: that is,
x, y
, it must be the case that x \leq y
or y \leq x
holds.x, y, z
, it must be the case that x \leq y
and y \leq z
imply x \leq z
;Let us write x \equiv y
when x \leq y
and y \leq x
hold. In that case, we say that x
and y
are equivalent.
Let us write x < y
when x \leq y
and \neg (y \leq x)
hold.
compare
must behave as follows:
x \equiv y
holds then compare x y
must be zero;x < y
holds then compare x y
must be negative;y < x
holds then compare x y
must be positive.If equivalence implies equality (that is, if for all elements x, y
, x \equiv y
implies x = y
) then we say that the relation \leq
is a total order.