		Search-engine friendly clone of the ACL2 documentation.

Components-of-the-environment-field

Env-write

Signature
(env-write env x86) → x86

Definitions and Theorems

Function: env-write$notinline

(defun env-write$notinline (env x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (env-alistp env)))
  (let ((__function__ 'env-write))
    (declare (ignorable __function__))
    (env-write-logic env x86)))

Theorem: x86p-env-write

(defthm x86p-env-write
  (implies (and (x86p x86) (env-alistp env))
           (x86p (env-write env x86))))