I-LIMITED

ACL2(r) recognizer for limited numbers 
Major Section:  REAL

(I-limited x) is true if and only if x is a number that is not infinitely large. This predicate is only defined in ACL2(r) (see real).