		Search-engine friendly clone of the ACL2 documentation.

Virtualization-for-validation

Write-bytes

Signature
(write-bytes bytes channel state) → state

Definitions and Theorems

Function: write-bytes

(defun write-bytes (bytes channel state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'write-bytes))
    (declare (ignorable __function__))
    (b* (((when (not bytes)) state)
         ((cons b tail) bytes)
         (state (write-byte$ b channel state)))
      (write-bytes tail channel state))))