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).