		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Logcdr

All but the least significant bit of a number.

Signature
(logcdr i) → int
Arguments: i — Guard (integerp i).
Returns: 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

Function: logcdr$inline

(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)))))

Theorem: logcdr-type

(defthm logcdr-type
  (b* ((int (logcdr$inline i)))
    (integerp int))
  :rule-classes :type-prescription)

Subtopics

Logcdr-default: Behavior of logcdr on bad inputs.
Logcdr-basics