Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
No other cites to report in NuprlPrimitives
sfa_doc_factorial
Def
x
! == if
x
=
0
1 else
x
(
x
-1)! fi (recursive)
Thm*
x
:
.
x
!
eq_int
Def
i
=
j
== if
i
=
j
true
; false
fi
Thm*
i
,
j
:
. (
i
=
j
)
Syntax:
x
!
has structure:
sfa_doc_factorial(
x
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc