Def is_num_rep
Def == m:. P:
Def == m:. ((P(zero_rep))(n:. (P(n))(P(suc_rep(n)))))(P(m))

is mentioned

In prior sections: hol num

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html