Convert a natural number into a string with the given width.
Similar to nat-to-dec-string but produces a fixed number of decimal digits. If the input number is smaller it is padded with 0s, and if larger its more-significant bits are truncated.
Function:
(defun nat-to-dec-string-width (n width) (declare (xargs :guard (and (natp n) (posp width)))) (let ((acl2::__function__ 'nat-to-dec-string-width)) (declare (ignorable acl2::__function__)) (b* ((width (mbe :logic (if (posp width) width 1) :exec width)) (chars (nat-to-dec-chars n)) (width-chars (cond ((<= width (len chars)) (nthcdr (- (len chars) width) chars)) (t (append (make-list (- width (len chars)) :initial-element #\0) chars))))) (implode width-chars))))
Theorem:
(defthm stringp-of-nat-to-dec-string-width (b* ((str (nat-to-dec-string-width n width))) (stringp str)) :rule-classes :type-prescription)
Theorem:
(defthm dec-digit-char-list*p-of-nat-to-dec-string-width (dec-digit-char-list*p (explode (nat-to-dec-string-width n width))))
Theorem:
(defthm nat-to-dec-string-width-nonempty (not (equal (nat-to-dec-string-width n width) "")))