STANDARD-PART

ACL2(r) function mapping limited numbers to standard numbers 
Major Section:  REAL

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