Lift make-numbered-name to lists.
(make-numbered-name-list bases indices/wildcards wrld) → names
Function:
(defun make-numbered-name-list (bases indices/wildcards wrld) (declare (xargs :guard (and (symbol-listp bases) (nat-listp indices/wildcards) (plist-worldp wrld)))) (declare (xargs :guard (= (len bases) (len indices/wildcards)))) (let ((__function__ 'make-numbered-name-list)) (declare (ignorable __function__)) (cond ((endp bases) nil) (t (cons (make-numbered-name (car bases) (car indices/wildcards) wrld) (make-numbered-name-list (cdr bases) (cdr indices/wildcards) wrld))))))
Theorem:
(defthm symbol-listp-of-make-numbered-name-list (b* ((names (make-numbered-name-list bases indices/wildcards wrld))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm len-of-make-numbered-name-list (b* ((?names (make-numbered-name-list bases indices/wildcards wrld))) (equal (len names) (len bases))))