		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