Standardp
ACL2(r) recognizer for standard objects
(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).
