hol list 2 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def map2 == f:'a'bl1:'al2:'b. map2(f;l1;l2)

is mentioned by

Thm* 'a,'b,'c:S.
Thm* and
Thm* (all(f:'a  'b  'c. equal(map2(f,nil,nil),nil))
Thm* ,all
Thm* ,(f:'a
Thm* ,( 'b
Thm* ,( 'c. all
Thm* ,( 'c(h1:'a. all
Thm* ,( 'c. (h1:'a(t1:hlist
Thm* ,( 'c. (h1:'a. (('a). all
Thm* ,( 'c. (h1:'a. (('a). (h2:'b. all
Thm* ,( 'c. (h1:'a. (('a). (h2:'b(t2:hlist('b). equal
Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (map2
Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ((f
Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (,cons(h1,t1)
Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (,cons(h2,t2))
Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,cons
Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,(f(h1,h2)
Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,,map2(f,t1,t2)))))))))
[hmap2_wd]

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

hol list 2 Sections HOLlib Doc