ACL2(r) function mapping limited numbers to standard numbers
(Standard-part x) is, for a given i-limited number x, the unique real number infinitesimally close (see i-close) to x. This function is only defined in ACL2(r) (see real).
