Complex/complex-rationalp
Recognizer for complex numbers
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.
