		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Nat-size

How many characters are required to represent a natural number?

Signature
(nat-size x print-base) → size
Arguments: x — Guard (natp x).; print-base — Guard (print-base-p print-base).
Returns: size — Type (posp size).

Definitions and Theorems

Function: nat-size$inline

(defun nat-size$inline (x print-base)
  (declare (xargs :guard (and (natp x)
                              (print-base-p print-base))))
  (let ((acl2::__function__ 'nat-size))
    (declare (ignorable acl2::__function__))
    (case (the (unsigned-byte 5) print-base)
      (10 (nat-to-dec-string-size x))
      (16 (nat-to-hex-string-size x))
      (8 (nat-to-oct-string-size x))
      (otherwise (nat-to-bin-string-size x)))))

Theorem: posp-of-nat-size

(defthm posp-of-nat-size
  (b* ((size (nat-size$inline x print-base)))
    (posp size))
  :rule-classes :type-prescription)