		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-dec-digit-achar

Print an ACL2 decimal digit character after preprocessing.

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

We turn the character into its code and print it. Note that we do not need the numeric value of the character; we just need to print the character itself.

Definitions and Theorems

Function: pprint-dec-digit-achar

(defun pprint-dec-digit-achar (achar bytes)
  (declare (xargs :guard (and (dec-digit-char-p achar)
                              (byte-listp bytes))))
  (pprint-char (char-code achar) bytes))

Theorem: byte-listp-of-pprint-dec-digit-achar

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