		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-hex-digit-achars

Print zero or more ACL2 hexadecimal digit characters after preprocessing.

Signature
(pprint-hex-digit-achars achars bytes) → new-bytes
Arguments: achars — Guard (hex-digit-char-listp achars).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

Definitions and Theorems

Function: pprint-hex-digit-achars

(defun pprint-hex-digit-achars (achars bytes)
  (declare (xargs :guard (and (hex-digit-char-listp achars)
                              (byte-listp bytes))))
  (b* (((when (endp achars))
        (byte-list-fix bytes))
       (bytes (pprint-hex-digit-achar (car achars)
                                      bytes)))
    (pprint-hex-digit-achars (cdr achars)
                             bytes)))

Theorem: byte-listp-of-pprint-hex-digit-achars

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