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

is mentioned by

Thm* f:(T1T2), Q:(T2), L:T1 List. Thm* filter(Q;map(f;L)) = map(f;filter(Q o f;L))	[filter_map]
Thm* a:T List, x:T', f:(TT'). (x  map(f;a))  (y:T. (y  a) & x = f(y))	[member_map]
Thm* a:T List, f:(TT). (x:T. (x  a)  f(x) = x)  map(f;a) = a	[trivial_map]
Thm* a:T List, f,g:(TT'). Thm* (x:T. (x  a)  f(x) = g(x))  map(f;a) = map(g;a)	[map_equal2]
Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||	[map_length_nat]
Thm* a:T List, f,g:(TT'). Thm* (i:. i<||a||  f(a[i]) = g(a[i]))  map(f;a) = map(g;a)	[map_equal]
Thm* f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as'))	[map_append_sq]
Def unzip(as) == <map(p.1of(p);as),map(p.2of(p);as)>	[unzip]

In prior sections: list 1

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