`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.