		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-dec-const

Pretty-print a decimal constant.

Signature
(pprint-dec-const n) → part
Arguments: n — Guard (natp n).
Returns: part — Type (msgp part).

According to the grammar [C:6.4.4.1], a `decimal constant' is a sequence of decimal digits that does not start with 0; with the optional suffixes, this becomes an integer constant. As noted in iconst, we allow 0 here, which is turned into the single digit 0.

Definitions and Theorems

Function: pprint-dec-const

(defun pprint-dec-const (n)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'pprint-dec-const))
    (declare (ignorable __function__))
    (str::nat-to-dec-string (lnfix n))))

Theorem: msgp-of-pprint-dec-const

(defthm msgp-of-pprint-dec-const
  (b* ((part (pprint-dec-const n)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-dec-const-of-nfix-n

(defthm pprint-dec-const-of-nfix-n
  (equal (pprint-dec-const (nfix n))
         (pprint-dec-const n)))

Theorem: pprint-dec-const-nat-equiv-congruence-on-n

(defthm pprint-dec-const-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (pprint-dec-const n)
                  (pprint-dec-const n-equiv)))
  :rule-classes :congruence)