		Search-engine friendly clone of the ACL2 documentation.

Fms!-lst

Write each object in a list to a character output channel.

General Form:

(fms!-lst list channel state)

where list is an arbitrary list that is null-terminated — that is, satisfies true-listp — channel is an open character output channel (see io), and state is the ACL2 state. This function simply prints each form in the given list, in order, without evisceration (see evisc-tuple), where each is printed with fms! as shown below.

Function: fms!-lst

(defun fms!-lst (lst chan state)
  (declare
       (xargs :stobjs state
              :guard (and (open-output-channel-p chan
                                                 :character state)
                          (true-listp lst))))
  (cond ((endp lst) state)
        (t (pprogn (fms! "~X01"
                         (list (cons #\0 (car lst))
                               (cons #\1 nil))
                         chan state nil)
                   (fms!-lst (cdr lst) chan state)))))