Def hnum == 

is mentioned by

Thm* 'a:S.  Thm* all Thm* (P:hlist('a)  hbool. equal Thm* (P:hlist('a)  hbool. (all Thm* (P:hlist('a)  hbool. ((l:hlist('a). implies(equal(length(l),0),P(l))) Thm* (P:hlist('a)  hbool. ,P(nil)))	[hlength_eq_nil]
Thm* 'a:S.  Thm* all Thm* (P:hlist('a) Thm* ( hbool. all Thm* ( hbool. (n:hnum. equal Thm* ( hbool. (n:hnum. (all Thm* ( hbool. (n:hnum. ((l:hlist('a). implies(equal(length(l),suc(n)),P(l))) Thm* ( hbool. (n:hnum. ,all Thm* ( hbool. (n:hnum. ,(l:hlist('a). implies Thm* ( hbool. (n:hnum. ,(l:hlist('a). (equal(length(l),n) Thm* ( hbool. (n:hnum. ,(l:hlist('a). ,(l:hlist('a). all Thm* ( hbool. (n:hnum. ,(l:hlist('a). ,(l:hlist('a). (x:'a. P(cons(x,l)))) Thm* ( hbool. (n:hnum. ,(l:hlist('a). ,(l))))))	[hlength_eq_cons]
Thm* 'a:S.  Thm* all Thm* (l:hlist('a). all Thm* (l:hlist('a). (n:hnum. equal Thm* (l:hlist('a). (n:hnum. (equal(length(l),suc(n)) Thm* (l:hlist('a). (n:hnum. ,exists Thm* (l:hlist('a). (n:hnum. ,(h:'a. exists Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). and Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). (equal(length(l'),n) Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,equal Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,(l Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,,cons(h,l'))))))))	[hlength_cons_2]
Thm* 'a:S. all(l:hlist('a). equal(equal(length(l),0),equal(l,nil)))	[hlength_nil_2]
Thm* 'a:S.  Thm* all Thm* (l:hlist('a). all Thm* (l:hlist('a). (P:'a  hbool. equal Thm* (l:hlist('a). (P:'a  hbool. (every(P,l) Thm* (l:hlist('a). (P:'a  hbool. ,all Thm* (l:hlist('a). (P:'a  hbool. ,(n:hnum. implies Thm* (l:hlist('a). (P:'a  hbool. ,(n:hnum. (lt(n,length(l)) Thm* (l:hlist('a). (P:'a  hbool. ,(n:hnum. ,P(el(n,l)))))))	[hevery_el]
Thm* 'b,'a:S. Thm* all(l:hlist('a). all(f:'a  'b. equal(length(map(f,l)),length(l))))	[hlength_map]
Thm* 'a:S.  Thm* all Thm* (l1:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). equal Thm* (l1:hlist('a). (l2:hlist('a). (length(append(l1,l2)) Thm* (l1:hlist('a). (l2:hlist('a). ,add(length(l1),length(l2)))))	[hlength_append_2]
Thm* 'a:S.  Thm* and Thm* (all(l:hlist('a). equal(el(0,l),hd(l))) Thm* ,all(l:hlist('a). all(n:hnum. equal(el(suc(n),l),el(n,tl(l))))))	[hel_wd]
Thm* 'a:S.  Thm* and Thm* (equal(length(nil),0) Thm* ,all(h:'a. all(t:hlist('a). equal(length(cons(h,t)),suc(length(t))))))	[hlength_wd]
Thm* and Thm* (equal(it_sum(nil),0) Thm* ,all Thm* ,(h:hnum. all(t:hlist(hnum). equal(it_sum(cons(h,t)),add(h,it_sum(t))))))	[hit_sum_wd]
Thm* 'a:S.  Thm* all Thm* (h:'a. all Thm* (h:'a. (t:hlist('a). equal Thm* (h:'a. (t:hlist('a). (cons(h,t) Thm* (h:'a. (t:hlist('a). ,abs_list Thm* (h:'a. (t:hlist('a). ,(pair Thm* (h:'a. (t:hlist('a). ,(((m:hnum. cond Thm* (h:'a. (t:hlist('a). ,(((m:hnum. (equal(m,0) Thm* (h:'a. (t:hlist('a). ,(((m:hnum. ,h Thm* (h:'a. (t:hlist('a). ,(((m:hnum. ,fst(rep_list(t),pre(m)))) Thm* (h:'a. (t:hlist('a). ,(,suc(snd(rep_list(t))))))))	[hcons_def]

In prior sections: hol num hol prim rec hol list 1

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