# Real

ACL2(r) support for real numbers

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.

ACL2(r) has the same source files as ACL2. After you download ACL2, you
can build ACL2(r) by executing the following command on the command line in
your acl2-sources directory, replacing <your_lisp> with a path to your
Lisp executable:

make large-acl2r LISP=<your_lisp>

This will create an executable in your acl2-sources directory named
saved_acl2r.

Note that if you have fetched the community-books, then you will
already have the books to be certified with ACL2(r). They can
be certified from your acl2-sources directory, shown here as <DIR>:

make regression ACL2=<DIR>/saved_acl2r

To check that you are running ACL2(r), 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.''

Caution: ACL2(r) should be considered experimental: although we (Kaufmann
and Moore) have carefully completed Gamboa's integration of the reals into the
ACL2 source code, our primary concern has been to ensure unchanged behavior
when ACL2 is compiled in the default manner, i.e., without the non-standard
extensions. As for every release of ACL2, at the time of a release we are
unaware of soundness bugs in ACL2 or ACL2(r).

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.

ACL2(r) does not currently support the useless-runes feature.

### Subtopics

- Standardp
- ACL2(r) recognizer for standard objects
- Standard-part
- ACL2(r) function mapping limited numbers to standard numbers
- I-limited
- ACL2(r) recognizer for limited numbers
- I-close
- ACL2(r) test for whether two numbers are infinitesimally close
- I-small
- ACL2(r) recognizer for infinitesimal numbers
- I-large
- ACL2(r) recognizer for infinitely large numbers
- Real-listp
- ACL2(r) recognizer for a true list of real numbers