		Search-engine friendly clone of the ACL2 documentation.

File-io-light

Write-bytes-to-file

Write bytes to a file.

;; Writes the BYTES to file FILENAME, overwriting its previous contents.
;; Returns (mv erp state).
(defund write-bytes-to-file (bytes filename ctx state)
  (declare (xargs :guard (and (all-bytep bytes)
                              (stringp filename))
                  :stobjs state))
  (mv-let (channel state)
    (open-output-channel filename :byte state)
    (if (not channel)
        (prog2$ (er hard? ctx "Unable to open file ~s0 for :byte output." filename)
                (mv t state))
      (pprogn (write-bytes-to-channel bytes channel state)
              (close-output-channel channel state)
              ;; no error:
              (mv nil state)))))