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

[Index]

HTML generated using lcpp2html.