		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Basic-print-nat

Print a natural number in a particular print base, no radix.

Signature
(basic-print-nat x base acc) → new-acc
Arguments: x — Guard (natp x).; base — Guard (print-base-p base).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: basic-print-nat

(defun basic-print-nat (x base acc)
  (declare (type unsigned-byte x)
           (type (unsigned-byte 5) base))
  (declare (xargs :guard (and (natp x) (print-base-p base))))
  (declare (xargs :split-types t))
  (let ((acl2::__function__ 'basic-print-nat))
    (declare (ignorable acl2::__function__))
    (case base
      (10 (revappend-nat-to-dec-chars x acc))
      (16 (revappend-nat-to-hex-chars x acc))
      (8 (revappend-nat-to-oct-chars x acc))
      (otherwise (revappend-nat-to-bin-chars x acc)))))

Theorem: character-listp-of-basic-print-nat

(defthm character-listp-of-basic-print-nat
  (implies (character-listp acc)
           (b* ((new-acc (basic-print-nat x base acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)