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**.

Thu Sep 14 08:45:18 EDT 1995