		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-univ-char-name

Print a universal character name after preprocessing.

Signature
(pprint-univ-char-name ucname bytes) → new-bytes
Arguments: ucname — Guard (univ-char-name-p ucname).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

Definitions and Theorems

Function: pprint-univ-char-name

(defun pprint-univ-char-name (ucname bytes)
  (declare (xargs :guard (and (univ-char-name-p ucname)
                              (byte-listp bytes))))
  (univ-char-name-case
       ucname :locase-u
       (b* ((bytes (pprint-astring "\\u" bytes))
            (bytes (pprint-hex-quad ucname.quad bytes)))
         bytes)
       :upcase-u
       (b* ((bytes (pprint-astring "\\U" bytes))
            (bytes (pprint-hex-quad ucname.quad1 bytes))
            (bytes (pprint-hex-quad ucname.quad2 bytes)))
         bytes)))

Theorem: byte-listp-of-pprint-univ-char-name

(defthm byte-listp-of-pprint-univ-char-name
  (b* ((new-bytes (pprint-univ-char-name ucname bytes)))
    (byte-listp new-bytes))
  :rule-classes :rewrite)