		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-escape

Print an escape sequence.

Signature
(pprint-escape esc bytes) → new-bytes
Arguments: esc — Guard (escapep esc).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

Definitions and Theorems

Function: pprint-escape

(defun pprint-escape (esc bytes)
  (declare (xargs :guard (and (escapep esc) (byte-listp bytes))))
  (escape-case
       esc :simple
       (pprint-simple-escape esc.escape bytes)
       :oct
       (pprint-oct-escape esc.escape bytes)
       :hex
       (b* ((bytes (pprint-astring "\\x" bytes))
            (bytes (pprint-hex-digit-achars esc.escape bytes)))
         bytes)
       :univ (pprint-univ-char-name esc.escape bytes)))

Theorem: byte-listp-of-pprint-escape

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