		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)))