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