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_factorial2
Def
x
!
== if
x
=
0
1 else
x
(
x
-2)!
fi (recursive)
Thm*
x
:{
x
:
| (
x
rem 2) = 0 }.
x
!
eq_int
Def
i
=
j
== if
i
=
j
true
; false
fi
Thm*
i
,
j
:
. (
i
=
j
)
Syntax:
x
!
has structure:
sfa_doc_factorial2(
x
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc