All but the least significant bit of a number.
(logcdr i) → int
- i — Guard (integerp i).
- int — Type (integerp int).
(logcdr i) is the cdr of an integer conceptualized as a
bit-vector, where the least significant bit is at the head of the list.
In languages like C, this might be written as i >> 1.
Definitions and Theorems
(defun logcdr$inline (i)
(declare (xargs :guard (integerp i)))
(let ((__function__ 'logcdr))
(declare (ignorable __function__))
(mbe :logic (ifloor i 2)
:exec (the integer (ash (the integer i) -1)))))
(b* ((int (logcdr$inline i)))
- Behavior of logcdr on bad inputs.