		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Logcar

Least significant bit of a number.

Signature
(logcar i) → bit
Arguments: i — Guard (integerp i).
Returns: bit — Type (bitp bit).

(logcar i) is the car 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: logcar$inline

(defun logcar$inline (i)
  (declare (xargs :guard (integerp i)))
  (let ((__function__ 'logcar))
    (declare (ignorable __function__))
    (mbe :logic (imod i 2)
         :exec (the (unsigned-byte 1)
                    (logand (the integer i) 1)))))

Theorem: logcar-type

(defthm logcar-type
 (b* ((bit (logcar$inline i)))
   (bitp bit))
 :rule-classes ((:type-prescription)
                (:generalize :corollary (or (equal (logcar i) 0)
                                            (equal (logcar i) 1)))))

Subtopics

Ihs/logcar-lemmas: Lemmas about logcar from the logops-lemmas book.
Logcar-default: Behavior of logcar on bad inputs.