Major Section: ACL2-BUILT-INS
For most ACL2 users, this is a macro abbreviating complex-rationalp;
see complex-rationalp. In ACL2(r) (see real), a complex number x may
have irrational real and imaginary parts. This macro abbreviates the
predicate complexp in ACL2(r), which holds for such x. Most ACL2
users can ignore this macro and use complex-rationalp instead. Some
community books use complex/complex-rationalp so that they are suitable
for ACL2(r) as well.
