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

<PRE>
List (E, C): <b>trait</b>
  % Add singleton and concatenation
  <b>includes</b> <A HREF="Deque.html">Deque</A>
  <b>introduces</b> 
    {__}: E -&gt; C
    __ || __: C, C -&gt; C
  <b>asserts</b> <b>forall</b> e: E, ls, ls1, ls2: C
    {e} == empty \postcat e;
    ls || empty == ls;
    ls1 || (ls2 \postcat e) == (ls1 || ls2) \postcat e
  <b>implies</b>
    C <b>generated</b> <b>by</b> empty, {__}, ||
    <b>converts</b> head, last, tail, init, len, {__}, ||
      exempting head(empty), last(empty),
        tail(empty), init(empty)
</PRE>

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