Def ncompose(f;n;x) == if n=0 then x else f(ncompose(f;n-1;x)) fi   (recursive)

is mentioned by

Thm* n:, x:'a, f:('a'a). n>0  ncompose(f;n;x) = f(ncompose(f;n-1;x))	[ncompose_pos]
Thm* f:('a'a), x:'a. ncompose(f;0;x) = x	[ncompose_zero]
Def rep_num == n:. ncompose(suc_rep;n;zero_rep)	[hrep_num]

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