		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-eprefix

Print an encoding prefix after preprocessing.

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

Definitions and Theorems

Function: pprint-eprefix

(defun pprint-eprefix (eprefix bytes)
  (declare (xargs :guard (and (eprefixp eprefix)
                              (byte-listp bytes))))
  (eprefix-case eprefix
                :locase-u8 (pprint-astring "u8" bytes)
                :locase-u (pprint-astring "u" bytes)
                :upcase-u (pprint-astring "U" bytes)
                :upcase-l (pprint-astring "L" bytes)))

Theorem: byte-listp-of-pprint-eprefix

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