Conjugate
Complex number conjugate
Conjugate takes an ACL2 number as an argument, and returns its
complex conjugate (i.e., the result of negating its imaginary part.).
Conjugate is a Common Lisp function. See any Common Lisp
documentation for more information.
Function: conjugate
(defun conjugate (x)
(declare (xargs :guard (acl2-numberp x)))
(complex (realpart x) (- (imagpart x))))
