		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Stat1->memory

Signature
(stat1->memory stat1) → memory
Arguments: stat1 — Guard (stat1p stat1).
Returns: memory — Type (stat1-memory-p memory), given (stat1p stat1).

Definitions and Theorems

Function: stat1->memory

(defun stat1->memory (stat1)
  (declare (xargs :stobjs (stat1)))
  (declare (xargs :guard (stat1p stat1)))
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'stat1->memory
                                     (list stat1))
          (let ((__function__ 'stat1->memory))
            (declare (ignorable __function__))
            (nth 2 stat1))))

Theorem: stat1-memory-p-of-stat1->memory

(defthm stat1-memory-p-of-stat1->memory
  (implies (stat1p stat1)
           (b* ((memory (stat1->memory stat1)))
             (stat1-memory-p memory)))
  :rule-classes :rewrite)