lt tag method should be leq (to work for partial orders)

[Reuben Thomas <rrt@...>]

The subject says it all, but here's an explanation: deducing >, >= and <=
from < doesn't work for partial orders. Consider the subset relation: the
current definition is that

a <= b iff not (b < a)

but it's false that "a is a subset of b iff b is not a proper subset of
a".

If you have an leq tag method instead, it works fine:

a < b iff a <= b and not (b <= a)

[What you wanted to do with lt was define

a <= b iff a < b and not a == b

but then you need an eq tag method too]

The only problem is that the definition about of < involves two
comparisons, while the current definitions involve only one. The way
around this would be to have an lt and an leq tag method, and to use the
two-comparison form only if the lt method isn't defined (and equivalently,
the form of <= that works only for total orders only if the leq tag mthod
isn't defined).

Hence my proposal is:

1. Add an "leq" tag method. [Whatever this translates to in 4.1
terminology.]

2. Use the following definitions:

If only lt defined, use the current defns.

If only leq defined, use

a < b iff a <= b and not (b <= a)
a > b iff b <= a and not (a <= b)
a >= b iff b <= a

If both defined, use

a > b iff b < a
a >= b iff b <= a


P.S. It would also be nice to have an eq tag method, and use the
following rules:

if there is an eq tag method, use it

if there is an leq tag method,

a == b iff a <= b and b <= a

This begs the question about how you then test reference equality.
Perhaps by adding === (for "is identical to")?

-- 
http://sc3d.org/rrt/ | free, a.  already paid for (Peyton Jones)