		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprinted-lines-to-channel

Write pretty-printed lines to a channel.

Signature
(pprinted-lines-to-channel lines channel state) → state
Arguments: lines — Guard (msg-listp lines).; channel — Guard (symbolp channel).

Definitions and Theorems

Function: pprinted-lines-to-channel

(defun pprinted-lines-to-channel (lines channel state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (msg-listp lines)
                              (symbolp channel))))
  (let ((__function__ 'pprinted-lines-to-channel))
    (declare (ignorable __function__))
    (b* (((when (endp lines)) state)
         ((mv & state)
          (fmt1! "~@0" (list (cons #\0 (car lines)))
                 0 channel state nil)))
      (pprinted-lines-to-channel (cdr lines)
                                 channel state))))