Major Section: PROGRAMMING
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 books in the ACL2 distribution use
complex/complex-rationalp so that they are suitable for ACL2(r) as
well.