Logbit
(logbit pos i) returns the bit of i at bit-position pos
as a bitp, 0 or 1.
- Signature
(logbit pos i) → bit
- Arguments
- pos — Guard (natp pos).
- i — Guard (integerp i).
- Returns
- bit — Type (bitp bit).
This is just like the Common Lisp function (logbitp pos i),
except that we return 1 or 0 (instead of t or nil).
In languages like C, this might be written as (i >> pos) & 1.
Definitions and Theorems
Function: logbit$inline
(defun logbit$inline (pos i)
(declare (xargs :guard (and (natp pos) (integerp i))))
(if (logbitp pos i) 1 0))
Theorem: logbit-type
(defthm logbit-type
(b* ((bit (logbit$inline pos i)))
(bitp bit))
:rule-classes :type-prescription)
Subtopics
- Ihs/logbitp-lemmas
- Lemmas about logbitp and logbit from the logops-lemmas book.
