		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-stringlit

Print a string literal after preprocessing.

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

Definitions and Theorems

Function: pprint-stringlit

(defun pprint-stringlit (stringlit bytes)
 (declare (xargs :guard (and (stringlitp stringlit)
                             (byte-listp bytes))))
 (b* (((stringlit stringlit) stringlit)
      (bytes (eprefix-option-case
                  stringlit.prefix?
                  :some (pprint-eprefix stringlit.prefix?.val bytes)
                  :none bytes))
      (bytes (pprint-astring "\"" bytes))
      (bytes (pprint-s-char-list stringlit.schars bytes))
      (bytes (pprint-astring "\"" bytes)))
   bytes))

Theorem: byte-listp-of-pprint-stringlit

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