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

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

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

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

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

if a=b s ; t fi
if a<b s ; 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:

Def i= j == if i=j true ; false fi
Def i< j == if i<j true ; false fi
Def i  j ==  j< i

Several Subtypes of are in common use.

Def   == {i: i 0 }
Def == {i: | 0 i }
Def  == {i: | 0<i }
Def {i...j} == {k: i k & k j }
Def {i..j } == {k: i k < j }

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

(March 2001 - sfa )