		Search-engine friendly clone of the ACL2 documentation.

Components-of-the-environment-field

Write-x86-file-contents

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

Definitions and Theorems

Function: write-x86-file-contents$notinline

(defun write-x86-file-contents$notinline (name contents x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (stringp name)))
  (let ((__function__ 'write-x86-file-contents))
    (declare (ignorable __function__))
    (write-x86-file-contents-logic name contents x86)))

Theorem: x86p-write-x86-file-contents

(defthm x86p-write-x86-file-contents
  (implies (and (x86p x86) (stringp name))
           (x86p (write-x86-file-contents name contents x86))))