		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-natural

Pretty-print a natural number.

Signature
(pprint-natural nat) → part
Arguments: nat — Guard (natp nat).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-natural

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

Theorem: msgp-of-pprint-natural

(defthm msgp-of-pprint-natural
  (b* ((part (pprint-natural nat)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-natural-of-nfix-nat

(defthm pprint-natural-of-nfix-nat
  (equal (pprint-natural (nfix nat))
         (pprint-natural nat)))

Theorem: pprint-natural-nat-equiv-congruence-on-nat

(defthm pprint-natural-nat-equiv-congruence-on-nat
  (implies (acl2::nat-equiv nat nat-equiv)
           (equal (pprint-natural nat)
                  (pprint-natural nat-equiv)))
  :rule-classes :congruence)