		Search-engine friendly clone of the ACL2 documentation.

Logops-byte-functions

Wrb

(wrb i bsp j) writes the (bsp-size bsp) low-order bits of i into the byte of j specified by bsp.

Signature
(wrb i bsp j) → int
Arguments: i — Guard (integerp i).; bsp — Guard (bspp bsp).; j — Guard (integerp j).
Returns: int — Type (integerp int).

This is analogous to Common Lisp's (dpb newbyte bytespec integer).

Definitions and Theorems

Function: wrb

(defun wrb (i bsp j)
  (declare (xargs :guard (and (integerp i)
                              (bspp bsp)
                              (integerp j))))
  (let ((__function__ 'wrb))
    (declare (ignorable __function__))
    (logapp (bsp-position bsp)
            (loghead (bsp-position bsp) j)
            (logapp (bsp-size bsp)
                    i
                    (logtail (+ (bsp-size bsp) (bsp-position bsp))
                             j)))))

Theorem: wrb-type

(defthm wrb-type
  (b* ((int (wrb i bsp j)))
    (integerp int))
  :rule-classes :type-prescription)

Subtopics

Ihs/wrb-lemmas