i
th bit of an integer
Major Section: ACL2-BUILT-INS
For a nonnegative integer i
and an integer j
, (logbitp i j)
is a
Boolean, which is t
if and only if the value of the i
th bit is 1
in the two's complement representation of j
.
(Logbitp i j)
has a guard that i
is a nonnegative integer and
j
is an integer.
Logbitp
is a Common Lisp function. See any Common Lisp
documentation for more information.
To see the ACL2 definition of this function, see pf.