		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-iconst

Pretty-print an integer constant.

Signature
(pprint-iconst c) → part
Arguments: c — Guard (iconstp c).
Returns: part — Type (msgp part).

If the constant is unsigned, we print the uppercase U, not the lowercase u.

Definitions and Theorems

Function: pprint-iconst

(defun pprint-iconst (c)
  (declare (xargs :guard (iconstp c)))
  (let ((__function__ 'pprint-iconst))
    (declare (ignorable __function__))
    (b* (((iconst c) c))
      (msg "~@0~@1~@2"
           (iconst-base-case c.base
                             :dec (pprint-dec-const c.value)
                             :oct (pprint-oct-const c.value)
                             :hex (pprint-hex-const c.value))
           (if c.unsignedp "U" "")
           (pprint-iconst-length c.length)))))

Theorem: msgp-of-pprint-iconst

(defthm msgp-of-pprint-iconst
  (b* ((part (pprint-iconst c)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-iconst-of-iconst-fix-c

(defthm pprint-iconst-of-iconst-fix-c
  (equal (pprint-iconst (iconst-fix c))
         (pprint-iconst c)))

Theorem: pprint-iconst-iconst-equiv-congruence-on-c

(defthm pprint-iconst-iconst-equiv-congruence-on-c
  (implies (iconst-equiv c c-equiv)
           (equal (pprint-iconst c)
                  (pprint-iconst c-equiv)))
  :rule-classes :congruence)