nil ; h.t if eq(x,h) t else h.remove(eq,x,t) fi) ) (eq,x,L)
T:Type, eq:(T
T
), x:T, L:T List. remove(eq;x;L) 
T List| Who Cites remove? | |
| remove | 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) |
| Thm* T:Type, eq:(TT), x:T, L:T List. remove(eq;x;L) T List | |
| 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) |
| Syntax: | remove(eq;x;L) | has structure: | remove(eq; x; L) |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |  |