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