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

<PRE>
IsTO (&lt;=, T): <b>trait</b>
  % &lt;<= is a total order on T
  <b>introduces</b> __&lt;=__: T, T -&gt; Bool
  <b>asserts</b> <b>forall</b> x, y, z: T
    x &lt;= x;
    (x &lt;= y /\ y &lt;= z) =&gt; x &lt;= z;
    x &lt;= y /\ y &lt;= x == x = y;
    x &lt;= y \/ y &lt;= x
  <b>implies</b> <A HREF="IsPO.html">IsPO</A>, <A HREF="TotalPreOrder.html">TotalPreOrder</A>
</PRE>

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