		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Wiml08

Signature
(wiml08 lin-addr val x86) → (mv * x86)

Definitions and Theorems

Function: wiml08

(defun wiml08 (lin-addr val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (signed-byte 48) lin-addr)
           (type (signed-byte 8) val))
  (declare (xargs :split-types t
                  :guard (and (canonical-address-p lin-addr)
                              (signed-byte-p 8 val))))
  (let ((__function__ 'wiml08))
    (declare (ignorable __function__))
    (wml08 lin-addr
           (the (unsigned-byte 8) (n08 val))
           x86)))

Theorem: x86p-wiml08

(defthm x86p-wiml08
  (implies (force (x86p x86))
           (x86p (mv-nth 1 (wiml08 lin-addr val x86))))
  :rule-classes (:rewrite :type-prescription))