Def map(f;as) == Case of as; nil  nil ; a.as'  cons((f(a)); map(f;as'))
Def (recursive)

is mentioned by

Thm* 'b,'a:S, l:'a List, f:('a'b). ||map(f;l)|| = ||l||	[length_map]
Thm* 'a,'b:S, f:('a'b), l1,l2:'a List. Thm* map(f;l1 @ l2) = (map(f;l1) @ map(f;l2))	[map_append_2]

In prior sections: list 1 hol list 1

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