		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-integer

Pretty-print an integer number.

Signature
(pprint-integer int) → part
Arguments: int — Guard (integerp int).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-integer

(defun pprint-integer (int)
  (declare (xargs :guard (integerp int)))
  (let ((__function__ 'pprint-integer))
    (declare (ignorable __function__))
    (str::int-to-dec-string int)))

Theorem: msgp-of-pprint-integer

(defthm msgp-of-pprint-integer
  (b* ((part (pprint-integer int)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-integer-of-ifix-int

(defthm pprint-integer-of-ifix-int
  (equal (pprint-integer (ifix int))
         (pprint-integer int)))

Theorem: pprint-integer-int-equiv-congruence-on-int

(defthm pprint-integer-int-equiv-congruence-on-int
  (implies (acl2::int-equiv int int-equiv)
           (equal (pprint-integer int)
                  (pprint-integer int-equiv)))
  :rule-classes :congruence)