The type of integers, int , is built
into Nuprl
.
The canonical members of this type are 
.
The operations of addition, +, subtraction, -,
multiplication, 
, and division, 
, are built into
the theory along with the modulus operation, 
,
which gives the positive remainder of dividing a by b.
Thus 
.
Division of two integers produces the integer
part of real number division, so 
.
For nonnegative integers a and b we have
.
There are three noncanonical forms associated
with the integers.
The first form captures the fact that integer
equality is decidable;
denotes s if 
and denotes t otherwise.
The second form captures the computational meaning
of less than; 
denotes s if a<b and
t otherwise.
The third form provides
a mechanism for definition and proof by induction and is written
.
It is easiest to see this form as a combination of two
simple induction forms over the nonnegative and nonpositive
integers.
Over the nonnegative integers (
) the form
denotes an inductive definition satisfying the following equations:
Over the nonpositive integers (
.
) the form denotes
an inductive definition satisfying these equations:
For example, this form could be used to define
.
as
if we assume that for 
.
In the form 
a represents the integer argument, b represents the value of
the form if a=0, 
represents the inductive case for negative
integers, and 
represents the inductive case for positive
integers.
The variables x and y are bound in s, while u and v are bound in t.
