		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-oct-digit

Pretty-print an octal digit.

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

Definitions and Theorems

Function: print-oct-digit

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

Theorem: msgp-of-print-oct-digit

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