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_factorial2Def x! == if x=0 1 else x(x-2)! fi  (recursive)
Thm* x:{x:| (x rem 2) = 0 }. x!  
eq_intDef i=j == if i=j true ; false fi
Thm* i,j:. (i=j 

Syntax:x! has structure: sfa_doc_factorial2(x)

About:
boolbfalsebtrueifthenelseintnatural_numbersubtractmultiplyremainder
int_eqsetrecursive_def_noticeequalmemberall
!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions NuprlPrimitives Sections NuprlLIB Doc