		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-chars

Print zero or more characters after preprocessing.

Signature
(pprint-chars chars bytes) → new-bytes
Arguments: chars — Guard (nat-listp chars).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

The characters are supplied in a list (of their codes). They are printed from left to right.

Definitions and Theorems

Function: pprint-chars

(defun pprint-chars (chars bytes)
  (declare (xargs :guard (and (nat-listp chars)
                              (byte-listp bytes))))
  (declare (xargs :guard (grammar-character-listp chars)))
  (b* (((when (endp chars))
        (byte-list-fix bytes))
       (bytes (pprint-char (car chars) bytes)))
    (pprint-chars (cdr chars) bytes)))

Theorem: byte-listp-of-pprint-chars

(defthm byte-listp-of-pprint-chars
  (b* ((new-bytes (pprint-chars chars bytes)))
    (byte-listp new-bytes))
  :rule-classes :rewrite)