the ith 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 ith 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.