Convert an integer into a string with a fixed number of digits.
Function:
(defun int-to-dec-string-width (i width) (declare (xargs :guard (and (integerp i) (posp width)))) (let ((acl2::__function__ 'int-to-dec-string-width)) (declare (ignorable acl2::__function__)) (b* ((i (mbe :logic (ifix i) :exec i)) (width (mbe :logic (if (posp width) width 1) :exec width)) (chars (if (< i 0) (b* ((chars (nat-to-dec-chars (- i)))) (cons #\- (cond ((<= width (len chars)) (nthcdr (- (len chars) width) chars)) (t (append (make-list (- width (len chars)) :initial-element #\0) chars))))) (b* ((chars (nat-to-dec-chars i))) (cond ((<= width (len chars)) (nthcdr (- (len chars) width) chars)) (t (append (make-list (- width (len chars)) :initial-element #\0) chars))))))) (implode chars))))
Theorem:
(defthm stringp-of-int-to-dec-string-width (b* ((str (int-to-dec-string-width i width))) (stringp str)) :rule-classes :type-prescription)
Theorem:
(defthm int-to-dec-string-width-nonempty (not (equal (int-to-dec-string-width i width) "")))