recognizer for complex numbers
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.