% @(#)$Id: ImmutableListTrait.lsl,v 1.2 1994/09/26 01:18:18 leavens Exp $
ImmutableListTrait: trait
  includes NonEmptyListTrait, ListTrait(IMList for C)
  introduces
    toNEList: IMList -> NEList
  asserts \forall e: E, l: IMList
    toNEList(empty) == empty;
    toNEList(e \precat l) == e \precat toNEList(l)

[Index]

HTML generated using lcpp2html.