Convert a list of integers into a list of strings.
(int-to-dec-string-list x) → strs
Function:
(defun int-to-dec-string-list (x) (declare (xargs :guard (integer-listp x))) (let ((acl2::__function__ 'int-to-dec-string-list)) (declare (ignorable acl2::__function__)) (if (atom x) nil (cons (int-to-dec-string (car x)) (int-to-dec-string-list (cdr x))))))
Theorem:
(defthm string-listp-of-int-to-dec-string-list (b* ((strs (int-to-dec-string-list x))) (string-listp strs)) :rule-classes :rewrite)
Theorem:
(defthm int-to-dec-string-list-when-atom (implies (atom x) (equal (int-to-dec-string-list x) nil)))
Theorem:
(defthm int-to-dec-string-list-of-cons (equal (int-to-dec-string-list (cons a x)) (cons (int-to-dec-string a) (int-to-dec-string-list x))))