		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-header-name

Print a header name after preprocessing.

Signature
(pprint-header-name header bytes) → new-bytes
Arguments: header — Guard (header-namep header).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

Definitions and Theorems

Function: pprint-header-name

(defun pprint-header-name (header bytes)
  (declare (xargs :guard (and (header-namep header)
                              (byte-listp bytes))))
  (header-name-case
       header :angles
       (b* ((bytes (pprint-astring "<" bytes))
            (bytes (pprint-h-char-list header.chars bytes))
            (bytes (pprint-astring ">" bytes)))
         bytes)
       :quotes
       (b* ((bytes (pprint-astring "\"" bytes))
            (bytes (pprint-q-char-list header.chars bytes))
            (bytes (pprint-astring "\"" bytes)))
         bytes)))

Theorem: byte-listp-of-pprint-header-name

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