Def filter(P;l) == reduce(a,v. if P(a) [a / v] else v fi;nil;l)

is mentioned by

Thm* P:(T), L2,L1:T List. L1  L2  filter(P;L1)  filter(P;L2)	[filter_iseg]
Thm* f:(T1T2), Q:(T2), L:T1 List. Thm* filter(Q;map(f;L)) = map(f;filter(Q o f;L))	[filter_map]
Thm* P:(T), l:T List. filter(P;l)  {x:T| P(x) } List	[filter_type]
Thm* P1,P2:(T), L:T List. Thm* filter(P1;filter(P2;L)) ~ filter(t.(P1(t))(P2(t));L)	[filter_filter]
Thm* P:(T), l1,l2:T List. filter(P;l1 @ l2) ~ (filter(P;l1) @ filter(P;l2))	[filter_append]
Thm* L:A List, f1,f2:(A). f1 = f2  (filter(f1;L) ~ filter(f2;L))	[filter_functionality]
Thm* P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x)	[member_filter]
Def (first x  as s.t. P(x) else d) Def == Case of filter(x.P(x);as); nil  d ; a.b  a	[find]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html