Convert an integer into a string with its digits.
For instance,
Function:
(defun int-to-dec-string$inline (i) (declare (xargs :guard (integerp i))) (let ((acl2::__function__ 'int-to-dec-string)) (declare (ignorable acl2::__function__)) (let ((i (mbe :logic (ifix i) :exec i))) (if (< i 0) (implode (cons #\- (nat-to-dec-chars (- i)))) (implode (nat-to-dec-chars i))))))
Theorem:
(defthm stringp-of-int-to-dec-string (b* ((str (int-to-dec-string$inline i))) (stringp str)) :rule-classes :type-prescription)
Theorem:
(defthm int-to-dec-string-nonempty (not (equal (int-to-dec-string i) "")))
Theorem:
(defthm int-to-dec-string-one-to-one-positive (equal (equal (int-to-dec-string n) (int-to-dec-string m)) (equal (ifix n) (ifix m))))