		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-oct-integer-literal

Pretty-print an octal integer literal.

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

Definitions and Theorems

Function: print-oct-integer-literal

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

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

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

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

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

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

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