Major Section: REAL
(Standardp x) is true if and only if x is a ``standard''
object. This notion of ``standard'' comes from non-standard analysis
and is discussed in Ruben Gamboa's dissertation. In brief, all the
familiar objects are standard: e.g., the familiar real numbers are
standard, but non-zero infinitesimals are not standard, and the familiar
integers are standard, but not those that exceed every integer that
you can express in the usual way (1, 2, 3, and so on). Similarly,
the familiar lists are standard, but not so a list that contains a
large number of integers, where ``large'' means more than the standard
integers. 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).
