		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-oct-escape

Print an octal escape after preprocessing.

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

Definitions and Theorems

Function: pprint-oct-escape

(defun pprint-oct-escape (esc bytes)
 (declare (xargs :guard (and (oct-escapep esc)
                             (byte-listp bytes))))
 (b*
  ((bytes (pprint-astring "\\" bytes))
   (bytes
        (oct-escape-case
             esc :one
             (pprint-oct-digit-achar esc.digit bytes)
             :two
             (b* ((bytes (pprint-oct-digit-achar esc.digit1 bytes))
                  (bytes (pprint-oct-digit-achar esc.digit2 bytes)))
               bytes)
             :three
             (b* ((bytes (pprint-oct-digit-achar esc.digit1 bytes))
                  (bytes (pprint-oct-digit-achar esc.digit2 bytes))
                  (bytes (pprint-oct-digit-achar esc.digit3 bytes)))
               bytes))))
  bytes))

Theorem: byte-listp-of-pprint-oct-escape

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