Real/rationalp
Recognizer for rational numbers (including real number in ACL2(r))
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 community books use real/rationalp so that these books
will be suitable for ACL2(r) as well.
