Print an integer in a particular print base, no radix.
(basic-print-int x base acc) → new-acc
Function:
(defun basic-print-int$inline (x base acc) (declare (type integer x) (type (unsigned-byte 5) base)) (declare (xargs :guard (and (integerp x) (print-base-p base)))) (declare (xargs :split-types t)) (let ((acl2::__function__ 'basic-print-int)) (declare (ignorable acl2::__function__)) (if (< x 0) (basic-print-nat (the unsigned-byte (- x)) base (cons #\- acc)) (basic-print-nat x base acc))))
Theorem:
(defthm character-listp-of-basic-print-int (implies (character-listp acc) (b* ((new-acc (basic-print-int$inline x base acc))) (character-listp new-acc))) :rule-classes :rewrite)