		Search-engine friendly clone of the ACL2 documentation.

Logandc1

Bitwise logical `and' of two ints, complementing the first

When integers are viewed in their two's complement representation, logandc1 returns the bitwise logical `and' of the second with the bitwise logical `not' of the first.

The guard for logandc1 requires its arguments to be integers. Logandc1 is defined in Common Lisp. See any Common Lisp documentation for more information.

Function: logandc1

(defun logandc1 (i j)
  (declare (xargs :guard (and (integerp i) (integerp j))))
  (logand (lognot i) j))