| | Who Cites disjoint2? |
|
| disjoint2 | 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) |
| | | Thm*  T:Type, eq:{T }, L,M:T List. disjoint(eq;L;M)  |
|
| is_member | 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) |
| | | Thm* T:Type, eq:(T  T), u:T. u(eq) nil |
| | | Thm* T:Type, eq:(TT), x:T, L:T List. x(eq) L |
|
| letrec_body | Def = b == b |
|
| letrec_arg | Def x b(x) (x) == b(x) |
|
| letrec | Def (letrec f b(f)) == b((letrec f b(f)) ) (recursive) |
