		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Logcons

(logcons b i) is the cons operation for integers, conceptualized as bit-vectors, where the least significant bit is at the head of the list.

Signature
(logcons b i) → int
Arguments: b — LSB of the result.
Guard (bitp b).; i — All but the LSB of the result.
Guard (integerp i).
Returns: int — Type (integerp int).

In languages like C, this might be written as (i << 1) + b.

Definitions and Theorems

Function: logcons$inline

(defun logcons$inline (b i)
  (declare (xargs :guard (and (bitp b) (integerp i))))
  (let ((__function__ 'logcons))
    (declare (ignorable __function__))
    (mbe :logic
         (let ((b (bfix b)) (i (ifix i)))
           (+ b (* 2 i)))
         :exec (the integer
                    (+ (the (unsigned-byte 1) b)
                       (the integer (ash i 1)))))))

Theorem: logcons-type

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

Subtopics

Ihs/logcons-lemmas: Basic lemmas relating logcons to logcar and logcdr, from the logops-lemmas book.
Logcons-basics