nil ; h.t if f(h) h.filter(f,t) else filter(f,t) fi) ) (f,L)
T:Type, f:(T
), L:T List. filter(f;L) 
T ListT:Type, f:(T), L:T List. filter(f;L) {x:T| f(x) } List| Who Cites filter? | |
| filter | 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) |
| Thm* T:Type, f:(T), L:T List. filter(f;L) T List | |
| Thm* T:Type, f:(T), L:T List. filter(f;L) {x:T| f(x) } 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: | filter(f;L) | has structure: | filter(f; L) |
About:
 |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |