		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-dec-integer-literal

Pretty-print a decimal integer literal.

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

Definitions and Theorems

Function: print-dec-integer-literal

(defun print-dec-integer-literal (lit)
  (declare (xargs :guard (dec-integer-literalp lit)))
  (let ((__function__ 'print-dec-integer-literal))
    (declare (ignorable __function__))
    (b* (((dec-integer-literal lit) lit))
      (msg "~@0~@1"
           (print-decdig/uscore-list lit.digits/uscores)
           (print-optional-integer-type-suffix lit.suffix?)))))

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

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

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

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

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

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