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