		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-bin-digit

Pretty-print a binary digit.

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

Definitions and Theorems

Function: print-bin-digit

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

Theorem: msgp-of-print-bin-digit

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