Def rep_num == n:. ncompose(suc_rep;n;zero_rep)

is mentioned by

Thm* all(m:hnum. equal(suc(m),abs_num(suc_rep(rep_num(m)))))	[hsuc_def]
Thm* and Thm* (all(a:hnum. equal(abs_num(rep_num(a)),a)) Thm* ,all(r:hind. equal(is_num_rep(r),equal(rep_num(abs_num(r)),r))))	[hnum_iso_def]
Thm* iso_pair(;;is_num_rep;rep_num;abs_num)	[num_iso]
Def abs_num == n:. @m:. (n = rep_num(m)  )	[habs_num]

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