[<A HREF="DerivedOrders.ps">PostScript</A>]

<PRE>
DerivedOrders (T): <b>trait</b>
  % Define any three of the comparison operators,
  % given the fourth
  <b>introduces</b>
    __&lt;=__, __&gt;=__, __&lt;__, __&gt;__: T, T -&gt; Bool
  <b>asserts</b> <b>forall</b> x, y: T
    x &lt;= y == x &lt; y \/ x = y;
    x &lt; y == x &lt;= y /\ ~(x = y);
    x &gt;= y == y &lt;= x;
    x &gt; y == y &lt; x
  <b>implies</b> 
    <b>converts</b> &gt;=, &lt;, &gt;
    <b>converts</b> &lt;=, &lt;, &gt;
    <b>converts</b> &lt;=, &gt;=, &gt;
    <b>converts</b> &lt;=, &gt;=, &lt;
</PRE>

[<A HREF="toc.html">Table of Contents</A>] [<A HREF="index.html">Index</A>]