		Search-engine friendly clone of the ACL2 documentation.

Bigmem

Write-mem$a

Signature
(write-mem$a addr val mem$a) → *
Arguments: mem$a — Guard (mem$ap mem$a).

Definitions and Theorems

Function: write-mem$a

(defun write-mem$a (addr val mem$a)
       (declare (type (unsigned-byte 64) addr)
                (type (unsigned-byte 8) val))
       (declare (xargs :guard (mem$ap mem$a)))
       (let ((__function__ 'write-mem$a))
            (declare (ignorable __function__))
            (ubp8-set addr val mem$a)))