IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Integers

is the type of integers; e.g. 1 and -1 .

The usual arithmetic operators that are primitive in this system are these:

-a a+b a-b ab ab a rem b

The following comparison operators happen also to be primitive in this system:

if a=bs ; t fi if a<bs ; t fi a<b

The two "conditionals" simply compare integers and take the appropriate branch. The "a<b" form represents the less-than relation on integers. See Propositions.

if 0=0 s ; t fi * s if 0=1 s ; t fi * t if 0<1 s ; t fi * s if 0<0 s ; t fi * t

There are also some often-used Boolean expressions for these integer relations:

Defi=j == if i=j true ; false fi Defi<j == if i<j true ; false fi Defij == j<i

"k" is an abbreviated display for {0..k}, which has been adopted as Nuprl's standard finite type with k elements.

Integer Literals

In Nuprl the canonical form for an integer is atomic, rather than, say, bit strings or iteration of successor from zero. There is a small complication involving the implementation of negative literals, which will be of interest only to those interested in reconciling the implementation with theory. See Negative Literals.