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