E.2.3 List

spec

List [Elem] =

free type

List[Elem] ::= nil | cons(first:?Elem; rest:?List[Elem])

op

__ ++ __ :

List[Elem]×List[Elem] -> List[Elem], assoc, unit nil

vars

e:Elem; l,l':List[Elem]

axiom

 
cons(e,l) ++ l' = cons(e,l ++ l')

op

reverse : List[Elem] -> List[Elem]

axioms

 
reverse(nil) = nil;
reverse(cons(e,l)) = reverse(l) ++ cons(e,nil)

end