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

<PRE>
Equality (T): <b>trait</b>
  % This trait is given for documentation only.
  % It is implicit in LSL.
  <b>introduces</b> __ = __, __ \neq __: T, T -&gt; Bool
  <b>asserts</b>
    T <b>partitioned</b> <b>by</b> =
    <b>forall</b> x, y, z: T
      x = x;
      x = y == y = x;
      (x = y /\ y = z) =&gt; x = z;
      x \neq y == ~(x = y)
  <b>implies</b> <A HREF="Equivalence.html">Equivalence</A> (= <b>for</b> \equiv)
</PRE>

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