(2steps total)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
modulus
wf
a
:
,
n
:
. (
a
mod
n
)
By:
Def of <int> mod <nat> THEN UnivCD
Generated subgoal:
1
1.
a
:
2.
n
:
if 0
a
a
rem
n
; ((-
a
) rem
n
)=
0
0 else
n
-((-
a
) rem
n
) fi
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
a:
, n:
. (a mod n) 
a:, n:. (a mod n)
if 0
a
a rem n ; ((-a) rem n)=0 0 else n-((-a) rem n) fi 
