Major Section: PROGRAMMING
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.