		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-integer-literal

Pretty-print an integer literal.

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

Definitions and Theorems

Function: print-integer-literal

(defun print-integer-literal (lit)
 (declare (xargs :guard (integer-literalp lit)))
 (let ((__function__ 'print-integer-literal))
   (declare (ignorable __function__))
   (integer-literal-case lit
                         :dec (print-dec-integer-literal lit.get)
                         :hex (print-hex-integer-literal lit.get)
                         :oct (print-oct-integer-literal lit.get)
                         :bin (print-bin-integer-literal lit.get))))

Theorem: msgp-of-print-integer-literal

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

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

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

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

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