Def map(f;as) == Case of as; nil  nil ; a.as'  [(f(a)) / map(f;as')]
Def (recursive)

is mentioned by

Thm* P:(AAProp), f:(BA), x,y:B List. Thm* (x swap adjacent[P(f(x),f(y))] y) Thm*  Thm* (map(f;x) swap adjacent[P(x,y)] map(f;y))	[swap_adjacent_map]
Thm* f:(AB), L1,L2:A List. L1  L2  map(f;L1)  map(f;L2)	[iseg_map]
Thm* f:(BA), x:B List, i,j:||x||. map(f;swap(x;i;j)) = swap(map(f;x);i;j)	[map_swap]
Thm* f:(AB), L:A List, P:(BProp). (xmap(f;L).P(x))  (xL.P(f(x)))	[l_all_map]
Def compose_flips(L) == compose_list(map(i.(i, i+1);L))	[compose_flips]
Def mapfilter(f;P;L) == map(f;filter(P;L))	[mapfilter]

In prior sections: list 1 mb list 1

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