Major Section: ACL2 Documentation

ACL2 supports rational numbers but not real numbers. However,
starting with Version 2.5, a variant of ACL2 called ``ACL2(r)''
supports the real numbers by way of non-standard analysis. ACL2(r)
was conceived and first implemented by Ruben Gamboa in his Ph.D.
dissertation work, supervised by Bob Boyer with active participation
by Matt Kaufmann. The makefile provided with ACL2 has targets
`small-acl2r`

and `large-acl2r`

for building ACL2(r) images. To see
which image you have, see if the prompt includes the string ```(r)`

'',
e.g.:

ACL2(r) !>Or, look at

`*acl2-version*`

and see if ```(r)`

'' is a substring.In ACL2 (as opposed to ACL2(r)), when we say ``real'' we mean ``rational.''

### I-CLOSE -- ACL2(r) test for whether two numbers are infinitesimally close

### I-LARGE -- ACL2(r) recognizer for infinitely large numbers

### I-LIMITED -- ACL2(r) recognizer for limited numbers

### I-SMALL -- ACL2(r) recognizer for infinitesimal numbers

### REAL-LISTP -- ACL2(r) recognizer for a true list of real numbers

### STANDARD-NUMBERP -- ACL2(r) recognizer for standard numbers

### STANDARD-PART -- ACL2(r) function mapping limited numbers to standard numbers

There is only limited documentation on the non-standard features of
ACL2(r). We hope to provide more documentation for such features in
future releases. Please feel free to query the authors if you are
interested in learning more about ACL2(r). Gamboa's dissertation
may also be helpful.

Major Section: REAL

`(I-close x y)`

is true if and only if `x-y`

is an infinitesimal number.
This predicate is only defined in ACL2(r) (see real).

Major Section: REAL

`(I-large x)`

is true if and only if `x`

is non-zero and `1/x`

is an
infinitesimal number. This predicate is only defined in ACL2(r)
(see real).

Major Section: REAL

`(I-limited x)`

is true if and only if `x`

is a number that is not
infinitely large. This predicate is only defined in ACL2(r)
(see real).

Major Section: REAL

`(I-small x)`

is true if and only if `x`

is an infinitesimal
number (possibly 0). This predicate is only defined in ACL2(r)
(see real).

Major Section: REAL

The predicate `real-listp`

tests whether its argument is a true
list of real numbers. This predicate is only defined in ACL2(r)
(see real).

Major Section: REAL

`(Standard-numberp x)`

is true if and only if `x`

is a ``standard''
number. This notion of ``standard'' comes from non-standard analysis
and is discussed in Ruben Gamboa's dissertation. In brief, all the
familiar real number are standard, but non-zero infinitesimals are
not standard, nor are numbers that exceed every integer that you can
express in the usual way (1, 2, 3, and so on). The set of standard
numbers is closed under the usual arithmetic operations, hence the
sum of a standard number and a non-zero infinitesimal is not
standard, though it is what is called ``limited''
(see i-limited).

This predicate is only defined in ACL2(r) (see real).

Major Section: REAL

`(Standard-part x)`

is, for a given `i-limited`

number `x`

, the unique
real number infinitesimally close (see i-close) to `x`

. This
function is only defined in ACL2(r) (see real).