% @(#)$Id: remove1stTrait.lsl,v 1.4 1997/07/25 05:32:45 leavens Exp $
remove1stTrait: trait
  includes ListTrait
  introduces
    without_first_occurrence_of: C, E -> C
  asserts \forall ls: C, e, e1: E
    without_first_occurrence_of(empty,e) == empty;
    without_first_occurrence_of(e \precat ls, e) == ls;
    without_first_occurrence_of(e1 \precat ls, e) ==
	e1 \precat without_first_occurrence_of(ls, e);

[Index]

HTML generated using lcpp2html.