Def rep_list == l:'a List. rep_list('a;l)

is mentioned by

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 list 1

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