		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-bin-integer-literal

Pretty-print a binary integer literal.

Signature
(print-bin-integer-literal lit) → part
Arguments: lit — Guard (bin-integer-literalp lit).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: print-bin-integer-literal

(defun print-bin-integer-literal (lit)
  (declare (xargs :guard (bin-integer-literalp lit)))
  (let ((__function__ 'print-bin-integer-literal))
    (declare (ignorable __function__))
    (b* (((bin-integer-literal lit) lit))
      (msg "~@0~@1~@2"
           (if lit.prefix-upcase-p "0B" "0b")
           (print-bindig/uscore-list lit.digits/uscores)
           (print-optional-integer-type-suffix lit.suffix?)))))

Theorem: msgp-of-print-bin-integer-literal

(defthm msgp-of-print-bin-integer-literal
  (b* ((part (print-bin-integer-literal lit)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: print-bin-integer-literal-of-bin-integer-literal-fix-lit

(defthm print-bin-integer-literal-of-bin-integer-literal-fix-lit
  (equal (print-bin-integer-literal (bin-integer-literal-fix lit))
         (print-bin-integer-literal lit)))

Theorem: print-bin-integer-literal-bin-integer-literal-equiv-congruence-on-lit

(defthm
 print-bin-integer-literal-bin-integer-literal-equiv-congruence-on-lit
 (implies (bin-integer-literal-equiv lit lit-equiv)
          (equal (print-bin-integer-literal lit)
                 (print-bin-integer-literal lit-equiv)))
 :rule-classes :congruence)