		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-iconst-length

Pretty-print a length suffix of integer constants.

Signature
(pprint-iconst-length ts) → part
Arguments: ts — Guard (iconst-lengthp ts).
Returns: part — Type (msgp part).

As noted in iconst-length, we use uppercase letters.

Definitions and Theorems

Function: pprint-iconst-length

(defun pprint-iconst-length (ts)
  (declare (xargs :guard (iconst-lengthp ts)))
  (let ((__function__ 'pprint-iconst-length))
    (declare (ignorable __function__))
    (iconst-length-case ts
                        :none ""
                        :long "L"
                        :llong "LL")))

Theorem: msgp-of-pprint-iconst-length

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

Theorem: pprint-iconst-length-of-iconst-length-fix-ts

(defthm pprint-iconst-length-of-iconst-length-fix-ts
  (equal (pprint-iconst-length (iconst-length-fix ts))
         (pprint-iconst-length ts)))

Theorem: pprint-iconst-length-iconst-length-equiv-congruence-on-ts

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