Major Section: REAL

(I-large x) is true if and only if x is non-zero and 1/x is an infinitesimal number. This predicate is only defined in ACL2(r) (see real).

(I-large x)

x

1/x