		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-q-char

Print a character usable in header names between double quotes after preprocessing.

Signature
(pprint-q-char qchar bytes) → new-bytes
Arguments: qchar — Guard (q-char-p qchar).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

Definitions and Theorems

Function: pprint-q-char

(defun pprint-q-char (qchar bytes)
  (declare (xargs :guard (and (q-char-p qchar)
                              (byte-listp bytes))))
  (let ((__function__ 'pprint-q-char))
    (declare (ignorable __function__))
    (b* ((code (q-char->code qchar))
         ((unless (grammar-character-p code))
          (raise "Internal error: bad character code ~x0."
                 code)))
      (pprint-char code bytes))))

Theorem: byte-listp-of-pprint-q-char

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