Prev Up Next
Go backward to E.2.5 Nat_List_with_Reverse_Orders
Go up to E.2 Generic Structured Specifications
Go forward to E.2.7 Path

E.2.6 Non_Empty_List

spec
Non_Empty_List [Elem] =
free type
NeList[Elem] ::= sort Elem | __ __(Elem; NeList[Elem])
ops
 
first : NeList[Elem] -> Elem;
rest : NeList[Elem] ->? NeList[Elem]
vars
e : Elem; l : NeList[Elem]
axioms
first(e) = e;         first(e l) = e;
¬ def rest(e);         rest(e l) = l
end

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk

Prev Up Next