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.