		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Logapp

(logapp size i j) is a binary append of i to j, where i effectively becomes the 'low' bits and j becomes the 'high' bits.

Signature
(logapp size i j) → int
Arguments: size — Guard (and (integerp size) (<= 0 size)).; i — Guard (integerp i).; j — Guard (integerp j).
Returns: int — Type (integerp int).

logapp is a specification for merging integers. Note that i is truncated to size bits before merging with j, and that j is shifted to the left by size bits before the merge.

Definitions and Theorems

Function: logapp

(defun logapp (size i j)
  (declare (type unsigned-byte size))
  (declare (xargs :guard (and (and (integerp size) (<= 0 size))
                              (integerp i)
                              (integerp j))))
  (declare (xargs :split-types t))
  (let ((__function__ 'logapp))
    (declare (ignorable __function__))
    (mbe :logic
         (let ((j (ifix j)))
           (+ (loghead size i) (* j (expt2 size))))
         :exec (+ (loghead size i) (ash j size)))))

Theorem: logapp-type

(defthm logapp-type
  (b* ((int (logapp size i j)))
    (integerp int))
  :rule-classes :type-prescription)

Subtopics

Ihs/logapp-lemmas: Lemmas about logapp from the logops-lemmas book.
Logapp*: Recursive definition of logapp.
Logapp-basics