		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Int-size

How many characters are required to represent an integer?

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

Definitions and Theorems

Function: int-size

(defun int-size (x print-base)
  (declare (xargs :guard (and (integerp x)
                              (print-base-p print-base))))
  (let ((acl2::__function__ 'int-size))
    (declare (ignorable acl2::__function__))
    (if (< x 0)
        (+ 1 (nat-size (- x) print-base))
      (nat-size x print-base))))

Theorem: posp-of-int-size

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