Major Section: ACL2-BUILT-INS
(lognot i) is the two's complement bitwise
`not' of the integer
Lognot is actually defined by coercing its argument to an integer
(see ifix), negating the result, and then subtracting
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.