Major Section: PROGRAMMING Examples: (complex x 3) ; x + 3i,
where i is the principal square root of -1 (complex x y) ; x +
yi (complex x 0) ; same as x, for rational numbers xThe function
complextakes two rational number arguments and returns an ACL2
number. This number will be of type (complex rational)[as
defined in the Common Lisp language], except that if the second
argument is zero, then complexreturns its first argument. The
function complex-rationalpis a recognizer for complex rational
numbers, i.e. for ACL2 numbers that are not rational numbers.
The reader macro #C (which is the same as #c) provides a
convenient way for typing in complex numbers. For explicit
rational numbers #C(x y) is read to the same value as (complex x
y). imagpart return the real and imaginary parts (respectively)
of a complex (possibly rational) number. So (realpart #C(3 4)) =
3, (imagpart #C(3 4)) = 4, (realpart 3/4) = 3/4, and (imagpart
3/4) = 0. The following built-in axiom may be useful for
reasoning about complex numbers.