Major Section: ACL2-BUILT-INS
(lognot i) is the two's complement bitwise `not' of the integer i.
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 integer.
Lognot is a Common Lisp function. See any Common Lisp
documentation for more information.
To see the ACL2 definition of this function, see pf.
