a,v. if P(a)
[a / v] else v fi;nil;l)
T:Type, P:(T
), l:T List. filter(P;l) 
T List k ; a.as' f(a,reduce(f;k;as')) (recursive)A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B| Who Cites filter? | |
| filter | Def filter(P;l) == reduce(a,v. if P(a) [a / v] else v fi;nil;l) |
| Thm* T:Type, P:(T), l:T List. filter(P;l) T List | |
| reduce |
Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) (recursive) |
|
Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B |
| Syntax: | filter(P;l) | has structure: | filter(P; l) |
About:
 |  |  |  |
 |  |  |  |  |
 |  |  |  |  |