// @(#)$Id: remove1st.h,v 1.5 1998/09/23 02:14:31 ruby Exp $

#ifndef remove1st_h
#define remove1st_h

#include "List.h"

template <class T /*@ expects contained_objects(T) @*/ >
List<T>* remove1st(List<T>* l, T e) throw();
//@ behavior {
//@   uses ListTrait(T for E, List<T> for C),
//@        remove1stTrait(T for E, List<T> for C);
//@   requires isValid(l);
//@   ensures (*result)' = without_first_occurrence_of((*l)\any, e);
//@ }

#endif

[Index]

HTML generated using lcpp2html.