		Search-engine friendly clone of the ACL2 documentation.

Numbered-names

Make-numbered-name-list

Lift make-numbered-name to lists.

Signature
(make-numbered-name-list bases indices/wildcards wrld) → names
Arguments: bases — Guard (symbol-listp bases).; indices/wildcards — Guard (nat-listp indices/wildcards).; wrld — Guard (plist-worldp wrld).
Returns: names — Type (symbol-listp names).

Definitions and Theorems

Function: make-numbered-name-list

(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: symbol-listp-of-make-numbered-name-list

(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: len-of-make-numbered-name-list

(defthm len-of-make-numbered-name-list
  (b*
   ((?names (make-numbered-name-list bases indices/wildcards wrld)))
   (equal (len names) (len bases))))