Def disjoint (eq;L;M) == (letrec disjoint2 L = (Case of L; nil  true ; h.t if h( eq) M false else disjoint2(t) fi) ) (L) | [disjoint2] |
Def  xL.P(x) == (letrec exists L = (Case of L; nil false ; h.t P(h)  exists(t)) ) (L) | [list_exists_2] |
| Def xL.P(x) == (letrec list_exists L = (Case of L; nil False ; h.t P(h) list_exists(t)) ) (L) | [list_exists] |
Def  xL.P(x) == (letrec all L = (Case of L; nil true ; h.t P(h) (all(t))) ) (L) | [list_all_2] |
| Def xL.P(x) == (letrec list_all L = (Case of L; nil True ; h.t P(h) & list_all(t)) ) (L) | [list_all] |
| Def x(eq) L == (letrec is_member x eq L = (Case of L; nil false ; h.t if eq(x,h) true else is_member(x,eq,t) fi) ) (x,eq,L) | [is_member] |
| Def filter(f;L) == (letrec filter f L = (Case of L; nil nil ; h.t if f(h) h.filter(f,t) else filter(f,t) fi) ) (f,L) | [filter] |
| Def remove(eq;x;L) == (letrec remove eq x L = (Case of L; nil nil ; h.t if eq(x,h) t else h.remove(eq,x,t) fi) ) (eq,x,L) | [remove] |
Def | | == (letrec l L = (Case of L; nil 0 ; h.t 1+l(t)) ) | [list_length] |