		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-iconst

Print an integer constant.

Signature
(print-iconst iconst pstate) → new-pstate
Arguments: iconst — Guard (iconstp iconst).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

Definitions and Theorems

Function: print-iconst

(defun print-iconst (iconst pstate)
  (declare (xargs :guard (and (iconstp iconst)
                              (pristatep pstate))))
  (let ((__function__ 'print-iconst))
    (declare (ignorable __function__))
    (b* (((iconst iconst) iconst)
         (pstate (print-dec/oct/hex-const iconst.core pstate))
         (pstate (print-isuffix-option iconst.suffix? pstate)))
      pstate)))

Theorem: pristatep-of-print-iconst

(defthm pristatep-of-print-iconst
  (b* ((new-pstate (print-iconst iconst pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-iconst-of-iconst-fix-iconst

(defthm print-iconst-of-iconst-fix-iconst
  (equal (print-iconst (iconst-fix iconst)
                       pstate)
         (print-iconst iconst pstate)))

Theorem: print-iconst-iconst-equiv-congruence-on-iconst

(defthm print-iconst-iconst-equiv-congruence-on-iconst
  (implies (iconst-equiv iconst iconst-equiv)
           (equal (print-iconst iconst pstate)
                  (print-iconst iconst-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-iconst-of-pristate-fix-pstate

(defthm print-iconst-of-pristate-fix-pstate
  (equal (print-iconst iconst (pristate-fix pstate))
         (print-iconst iconst pstate)))

Theorem: print-iconst-pristate-equiv-congruence-on-pstate

(defthm print-iconst-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-iconst iconst pstate)
                  (print-iconst iconst pstate-equiv)))
  :rule-classes :congruence)