		Search-engine friendly clone of the ACL2 documentation.

Logbitp

The ith bit of an integer

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.

Function: logbitp

(defun logbitp (i j)
  (declare (xargs :guard (and (integerp j)
                              (integerp i)
                              (>= i 0))))
  (oddp (floor (ifix j) (expt 2 (nfix i)))))

Subtopics

Open-logbitp-of-const-meta: Rewrite terms like (logbitp foo 7) to (or (not (natp foo)) (member-equal foo '(0 1 2))).
Ihs/logbitp-lemmas: Lemmas about logbitp and logbit from the logops-lemmas book.
Equal-by-logbitp: Show a = b by showing their bits are equal.
Logbit: (logbit pos i) returns the bit of i at bit-position pos as a bitp, 0 or 1.
Logbitp-mismatch: (logbitp-mismatch a b) finds the minimal bit-position for which a and b differ, or returns NIL if no such bit exists.
Logbitp-bounds: Lemmas about inferring logbitp information from bounds expressed using expt and vice versa
Logbitp-defaults: Behavior of logbitp on bad inputs.
Logbitp*: Recursive definition of logbitp.