STANDARD-NUMBERP

ACL2(r) recognizer for standard numbers
Major Section:  REAL

(Standard-numberp x) is true if and only if x is a ``standard'' number. This notion of ``standard'' comes from non-standard analysis and is discussed in Ruben Gamboa's dissertation. In brief, all the familiar real numbers are standard, but non-zero infinitesimals are not standard, nor are numbers that exceed every integer that you can express in the usual way (1, 2, 3, and so on). 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).