		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-c-char-list

Print a list of characters and escape sequences usable in character constants, after preprocessing.

Signature
(pprint-c-char-list cchars bytes) → new-bytes
Arguments: cchars — Guard (c-char-listp cchars).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

Definitions and Theorems

Function: pprint-c-char-list

(defun pprint-c-char-list (cchars bytes)
  (declare (xargs :guard (and (c-char-listp cchars)
                              (byte-listp bytes))))
  (b* (((when (endp cchars))
        (byte-list-fix bytes))
       (bytes (pprint-c-char (car cchars) bytes)))
    (pprint-c-char-list (cdr cchars)
                        bytes)))

Theorem: byte-listp-of-pprint-c-char-list

(defthm byte-listp-of-pprint-c-char-list
  (b* ((new-bytes (pprint-c-char-list cchars bytes)))
    (byte-listp new-bytes))
  :rule-classes :rewrite)