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))))