Major Section: ACL2-BUILT-INS
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.
