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

<PRE>
Conditional (T): <b>trait</b>
  % This trait is given for documentation only.
  % It is implicit in LSL.
  <b>introduces</b> if__<b>then</b>__<b>else</b>__: Bool, T, T -&gt; T
  <b>asserts</b>
    <b>forall</b> x, y, z: T
      <b>if</b> true <b>then</b> x <b>else</b> y == x;
      <b>if</b> false <b>then</b> x <b>else</b> y == y
  <b>implies</b> <b>forall</b> b: Bool, x: T
    <b>if</b> b <b>then</b> x <b>else</b> x == x
</PRE>

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