next up previous contents index
Next: Atoms and Lists Up: Extending the Typed Previous: Disjoint Union


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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995