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

is mentioned by

Thm* P:(AAProp), f:(A), L1,L2:A List. Thm* (L1 swap adjacent[P(x,y)] L2) Thm*  Thm* (filter(f;L1) swap adjacent[P(x,y)] filter(f;L2)) Thm*  filter(f;L1) = filter(f;L2)	[filter_swap_adjacent]
Thm* P:(T), l:T List. no_repeats(T;l)  no_repeats(T;filter(P;l))	[no_repeats_filter]
Thm* l:T List, P:(T), x,y:T. Thm* x before y  filter(P;l)  P(x) & P(y) & x before y  l	[l_before_filter]
Thm* L1,L2:T List, P:(T). L2  filter(P;L1)  L2  L1 & (xL2.P(x))	[sublist_filter]
Thm* P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ nil)	[filter_is_nil]
Thm* P:(T), L:T List. (xL.P(x))  filter(P;L) = L	[filter_trivial2]
Thm* P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ L)	[filter_trivial]
Def mapfilter(f;P;L) == map(f;filter(P;L))	[mapfilter]

In prior sections: mb list 1

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