NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
3
Thm*
Y(
f
,
x
. if
x
=
0
1 else
x
f
(
x
-1) fi)
[sfa_doc_ycomb_factorial_typing]
cites the following:
2
Thm*
i
,
j
:
.
i
j
[multiply_nat_wf]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
NuprlPrimitives
Sections
NuprlLIB
Doc
f,x. if x=
0
1 else x
f(x-1) fi) 
i,j:. ij f,x. if x=0 1 else xf(x-1) fi) i,j:. ij