		Search-engine friendly clone of the ACL2 documentation.

Virtualization-for-validation

Write-val1

Signature
(write-val1 size) → *

Definitions and Theorems

Function: write-val1

(defun write-val1 (size)
  (declare (xargs :guard t))
  (let ((__function__ 'write-val1))
    (declare (ignorable __function__))
    (if (equal size 0)
        nil
      (cons '((mv ?val state)
              (b* ((state (write-byte$ (logand 255 val)
                                       channel state)))
                (mv (ash val -8) state)))
            (write-val1 (- size 8))))))