		Search-engine friendly clone of the ACL2 documentation.

Bigmem

Read-mem$a

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

Definitions and Theorems

Function: read-mem$a

(defun read-mem$a (addr mem$a)
  (declare (type (unsigned-byte 64) addr))
  (declare (xargs :guard (mem$ap mem$a)))
  (let ((__function__ 'read-mem$a))
    (declare (ignorable __function__))
    (ubp8-get addr mem$a)))