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

<PRE>
IndexOp: <b>trait</b>
  % Select the i-th  element in the container
  % (in enumeration order).
  <b>assumes</b> <A HREF="Integer.html">Integer</A>, <A HREF="Container.html">Container</A>
  <b>introduces</b> __[__]: C, Int -&gt; E
  <b>asserts</b> <b>forall</b> c: C, i: Int
    c[0] == head(c);
    i &gt;= 0 =&gt; c[i+1] = tail(c)[i]
</PRE>

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