STANDARDP

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