List.MakeOrd
Functor building an implementation of Ord
given a totally ordered type. The ordering between two lists of totally ordered types is as follows with respect to compare l r
:
compare l r < 0
if the first non-equal comparison has the element in l
be less than the element in r
, or r
starts with l
.compare l r > 0
if the first non-equal comparison has the element in l
be greater than the element in r
, or l
starts with r
.compare l r = 0
if all elements in l
and r
are pairwise equal.compare a b
compares a
and b
for ordering.
compare a b < 0
if a
precedes b
(denoted a < b
),compare a b = 0
if a
is equal to b
(denoted a = b
),compare a b > 0
if a
succeeds b
(denoted a > b
).This should satisfy the following properties:
(compare a b <= 0 || compare b a >= 0) = true
,(compare a b <= 0) = true
and (compare b c <= 0) = true
, then (compare a c <= 0) = true
,(compare a a = 0) = true
,(compare a b <= 0) = true
and (compare a b >= 0) = true
then (compare a b = 0) = true
.