Major Section: ACL2-BUILT-INS
When integers are viewed in their two's complement representation,
logandc2
returns the bitwise logical `and' of the first with the
bitwise logical `not' of the second.
The guard for logandc2
requires its arguments to be integers.
Logandc2
is defined in Common Lisp. See any Common Lisp
documentation for more information.
To see the ACL2 definition of this function, see pf.