I-LARGE

ACL2(r) recognizer for infinitely large numbers 
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).