		Search-engine friendly clone of the ACL2 documentation.

Logops-byte-functions

Wrb-field

(wrb-field i bsp j) is analogous to Common Lisp's (deposit-field newbyte bytespec integer).

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

Definitions and Theorems

Function: wrb-field

(defun wrb-field (i bsp j)
  (declare (xargs :guard (and (integerp i)
                              (bspp bsp)
                              (integerp j))))
  (let ((__function__ 'wrb-field))
    (declare (ignorable __function__))
    (wrb (rdb bsp i) bsp j)))

Theorem: wrb-field-type

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