Bitwise not of a two's complement number
(lognot i) is the two's complement bitwise `not' of the
Lognot is actually defined by coercing its argument to an integer (see
ifix), negating the result, and then subtracting 1.
The guard for lognot requires its argument to be an
Lognot is a Common Lisp function. See any Common Lisp documentation
for more information.
(defun lognot (i)
(declare (xargs :guard (integerp i)))
(+ (- (ifix i)) -1))
- Lemmas about lognot from the logops-lemmas book.
- Recursive definition of lognot.
- Behavior of lognot on bad inputs.