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

is mentioned by

Thm* f:((T List)), t,t':. Thm* t<t'  concat(map(f;upto(t))) @ (f(t))  concat(map(f;upto(t')))	[concat_map_upto]
Thm* f:(TopTop), n:, l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l))	[firstn_map]
Thm* t',m:, T:Type, f:(T), P:(T). Thm* m+1||filter(P;map(f;upto(t')))|| Thm*  Thm* (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )	[filter_map_upto2]
Thm* i,j:. Thm* i<j Thm*  Thm* (f:(T), P:(T). Thm* (P(f(i))  ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(j)))||)	[filter_map_upto]
Thm* f:(TT'), L:T List, x',y':T'. Thm* x' before y'  map(f;L)  (x,y:T. x before y  L & f(x) = x' & f(y) = y')	[before-map]
Thm* m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))	[upto_decomp]
Thm* f:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i]))	[select-map]
Thm* f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L||	[length-map]
Thm* L:Top List. map(x.x;L) ~ L	[map-id]
Thm* f:(AB), l:A List. map(f;l) = nil  l = nil	[map_is_nil]
Thm* as:Top List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as)	[map-map]

In prior sections: list 1 mb list 1 mb list 2

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