LOGAND

bitwise logical `and' of zero or more integers
Major Section:  ACL2-BUILT-INS

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.