REAL/RATIONALP

recognizer for rational numbers (including real number in ACL2(r))
Major Section:  PROGRAMMING

For most ACL2 users, this is a macro abbreviating rationalp. In ACL2(r) (see real), this macro abbreviates the predicate realp, which holds for real numbers as well (including rationals). Most ACL2 users can ignore this macro and use rationalp instead, but many books in the ACL2 distribution use real/rationalp so that these books will be suitable for ACL2(r) as well.