		Search-engine friendly clone of the ACL2 documentation.

Decimal

Nat-to-dec-string-list

Convert a list of natural numbers into a list of strings.

Signature
(nat-to-dec-string-list x) → strs
Arguments: x — Guard (nat-listp x).
Returns: strs — Type (string-listp strs).

Definitions and Theorems

Function: nat-to-dec-string-list

(defun nat-to-dec-string-list (x)
  (declare (xargs :guard (nat-listp x)))
  (let ((acl2::__function__ 'nat-to-dec-string-list))
    (declare (ignorable acl2::__function__))
    (if (atom x)
        nil
      (cons (nat-to-dec-string (car x))
            (nat-to-dec-string-list (cdr x))))))

Theorem: string-listp-of-nat-to-dec-string-list

(defthm string-listp-of-nat-to-dec-string-list
  (b* ((strs (nat-to-dec-string-list x)))
    (string-listp strs))
  :rule-classes :rewrite)

Theorem: nat-to-dec-string-list-when-atom

(defthm nat-to-dec-string-list-when-atom
  (implies (atom x)
           (equal (nat-to-dec-string-list x) nil)))

Theorem: nat-to-dec-string-list-of-cons

(defthm nat-to-dec-string-list-of-cons
  (equal (nat-to-dec-string-list (cons a x))
         (cons (nat-to-dec-string a)
               (nat-to-dec-string-list x))))