		Search-engine friendly clone of the ACL2 documentation.

Components-of-the-environment-field

Write-x86-file-contents-logic

Signature
(write-x86-file-contents-logic name contents-field x86) → x86

Replacing the value associated with the name key by contents-field in the :FILE-CONTENTS field of the environment.

Definitions and Theorems

Function: write-x86-file-contents-logic

(defun write-x86-file-contents-logic (name contents-field x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (stringp name)))
 (let ((__function__ 'write-x86-file-contents-logic))
  (declare (ignorable __function__))
  (b*
   ((env (env-read x86))
    (file-contents-field (cdr (assoc-equal :file-contents env)))
    (x86
     (env-write
      (acons
       ':file-descriptors
       (cdr (assoc-equal :file-descriptors env))
       (acons
           ':file-contents
           (put-assoc-equal name contents-field file-contents-field)
           (acons ':oracle
                  (cdr (assoc-equal :oracle env))
                  nil)))
      x86)))
   x86)))