[PostScript]
List (E, C): trait
  % Add singleton and concatenation
  includes Deque
  introduces 
    {__}: E -> C
    __ || __: C, C -> C
  asserts forall e: E, ls, ls1, ls2: C
    {e} == empty \postcat e;
    ls || empty == ls;
    ls1 || (ls2 \postcat e) == (ls1 || ls2) \postcat e
  implies
    C generated by empty, {__}, ||
    converts head, last, tail, init, len, {__}, ||
      exempting head(empty), last(empty),
        tail(empty), init(empty)
[Table of Contents] [Index]