ith bit of an integer
Major Section: ACL2-BUILT-INS
For a nonnegative integer
i and an integer
(logbitp i j) is a
Boolean, which is
t if and only if the value of the
ith bit is
in the two's complement representation of
(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.