The numbers in ACL2 can be partitioned into the following subtypes:

Rationals Integers Positive integers`3`

Zero`0`

Negative Integers`-3`

Non-Integral Rationals Positive Non-Integral Rationals`19/3`

Negative Non-Integral Rationals`-22/7`

Complex Rational Numbers`#c(3 5/2) ; = 3+(5/2)i`

Signed integer constants are usually written (as illustrated above)
as sequences of decimal digits, possibly preceded by `+`

or `-`

.
Decimal points are not allowed. Integers may be written in binary,
as in `#b1011`

(= 23) and `#b-111`

(= -7). Octal may also be
used, `#o-777`

= -511. Non-integral rationals are written as a
signed decimal integer and an unsigned decimal integer, separated by
a slash. Complex rationals are written as #c(rpart ipart) where
rpart and ipart are rationals.

Of course, 4/2 = 2/1 = 2 (i.e., not every rational written with a slash is a non-integer). Similarly, #c(4/2 0) = #c(2 0) = 2.

The common arithmetic functions and relations are denoted by `+`

,
`-`

, `*`

, `/`

, `=`

, `<`

, `<=`

, `>`

and `>=`

. However there
are many others, e.g., `floor`

, `ceiling`

, and `lognot`

. We
suggest you see programming where we list all of the primitive
ACL2 functions. Alternatively, see any Common Lisp language
documentation.

The primitive predicates for recognizing numbers are illustrated below. The following ACL2 function will classify an object, x, according to its numeric subtype, or else return 'NaN (not a number). We show it this way just to illustrate programming in ACL2.

(defun classify-number (x) (cond ((rationalp x) (cond ((integerp x) (cond ((< 0 x) 'positive-integer) ((= 0 x) 'zero) (t 'negative-integer))) ((< 0 x) 'positive-non-integral-rational) (t 'negative-non-integral-rational))) ((complex-rationalp x) 'complex-rational) (t 'NaN)))