Also see Integers for newer supplementary material.
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.