		Search-engine friendly clone of the ACL2 documentation.

Grammar-printer-implementation

Pretty-print-number

Pretty-print a number in a given base.

Signature
(pretty-print-number nat base) → string
Arguments: nat — Guard (natp nat).; base — Guard (num-base-p base).
Returns: string — Type (common-lisp::stringp string).

We print numbers without leading zeros, except for a single zero if the number is 0. We might extend the abstract syntax to keep information about any leading zeros, in numeric value notations and in repetition prefixes.

Definitions and Theorems

Function: pretty-print-number

(defun pretty-print-number (nat base)
  (declare (xargs :guard (and (natp nat) (num-base-p base))))
  (let ((__function__ 'pretty-print-number))
    (declare (ignorable __function__))
    (num-base-case base
                   :dec (str::nat-to-dec-string nat)
                   :hex (str::nat-to-hex-string nat)
                   :bin (str::nat-to-bin-string nat))))

Theorem: stringp-of-pretty-print-number

(defthm stringp-of-pretty-print-number
  (b* ((string (pretty-print-number nat base)))
    (common-lisp::stringp string))
  :rule-classes :rewrite)