		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Wiml16

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

Definitions and Theorems

Function: wiml16

(defun wiml16 (lin-addr val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (signed-byte 48) lin-addr)
           (type (signed-byte 16) val))
  (declare (xargs :guard (canonical-address-p lin-addr)))
  (let ((__function__ 'wiml16))
    (declare (ignorable __function__))
    (wml16 lin-addr
           (the (unsigned-byte 16) (n16 val))
           x86)))

Theorem: x86p-wiml16

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