		Search-engine friendly clone of the ACL2 documentation.

File-io-light

Write-strings-to-channel

Write strings to an output channel.

;; Returns state.
(defund write-strings-to-channel (strings channel state)
  (declare (xargs :guard (and (string-listp strings)
                              (symbolp channel)
                              (open-output-channel-p channel :character state))
                  :stobjs state
                  :guard-hints (("Goal" :in-theory (enable open-output-channel-p)))))
  (if (endp strings)
      state
    (pprogn (princ$ (car strings) channel state) ;todo: call something faster? (e.g., something that only works for strings)?
            (write-strings-to-channel (cdr strings) channel state))))