		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-dec-digit

Pretty-print a decimal digit.

Signature
(print-dec-digit digit) → part
Arguments: digit — Guard (dec-digitp digit).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: print-dec-digit

(defun print-dec-digit (digit)
  (declare (xargs :guard (dec-digitp digit)))
  (let ((__function__ 'print-dec-digit))
    (declare (ignorable __function__))
    (implode (list (code-char digit)))))

Theorem: msgp-of-print-dec-digit

(defthm msgp-of-print-dec-digit
  (b* ((part (print-dec-digit digit)))
    (msgp part))
  :rule-classes :rewrite)