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