		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-hex-digit

Pretty-print a hexadecimal digit.

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

Definitions and Theorems

Function: print-hex-digit

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

Theorem: msgp-of-print-hex-digit

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