Module type Baby.OrderedType

The type of the set elements.

The function compare decides a relation \leq over elements of type t.

The relation \leq must be a total preorder: that is,

1. for all elements x, y, it must be the case that x \leq y or y \leq x holds.
2. for all elements 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:

1. if x \equiv y holds then compare x y must be zero;
2. if x < y holds then compare x y must be negative;
3. if 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.