		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-cconst

Print a character constant after preprocessing.

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

Definitions and Theorems

Function: pprint-cconst

(defun pprint-cconst (cconst bytes)
  (declare (xargs :guard (and (cconstp cconst)
                              (byte-listp bytes))))
  (b* (((cconst cconst) cconst)
       (bytes (cprefix-option-case
                   cconst.prefix?
                   :some (pprint-cprefix cconst.prefix?.val bytes)
                   :none bytes))
       (bytes (pprint-astring "'" bytes))
       (bytes (pprint-c-char-list cconst.cchars bytes))
       (bytes (pprint-astring "'" bytes)))
    bytes))

Theorem: byte-listp-of-pprint-cconst

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