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 (logand) expands to (logand x) expands to
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.