Major Section: ACL2-BUILT-INS
When integers are viewed in their two's complement representation,
logxor returns their bitwise logical exclusive or. In ACL2 logxor is a
macro that expands into calls of the binary function binary-logxor,
except that (logxor) expands to 0 and (logxor x) expands to x.
The guard for binary-logxor requires its arguments to be integers.
Logxor is defined in Common Lisp. See any Common Lisp
documentation for more information.
