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 target
`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.