		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-make-mv-nth-terms

Create a list of mv-nths applied to a term for a list of indices.

Signature
(atc-make-mv-nth-terms indices term) → terms
Arguments: indices — Guard (nat-listp indices).; term — Guard (pseudo-termp term).
Returns: terms — Type (pseudo-term-listp terms).

Definitions and Theorems

Function: atc-make-mv-nth-terms

(defun atc-make-mv-nth-terms (indices term)
 (declare (xargs :guard (and (nat-listp indices)
                             (pseudo-termp term))))
 (let ((__function__ 'atc-make-mv-nth-terms))
  (declare (ignorable __function__))
  (cond ((endp indices) nil)
        (t (cons (cons 'mv-nth
                       (cons (cons 'quote (cons (car indices) 'nil))
                             (cons (pseudo-term-fix term) 'nil)))
                 (atc-make-mv-nth-terms (cdr indices)
                                        term))))))

Theorem: pseudo-term-listp-of-atc-make-mv-nth-terms

(defthm pseudo-term-listp-of-atc-make-mv-nth-terms
  (b* ((terms (atc-make-mv-nth-terms indices term)))
    (pseudo-term-listp terms))
  :rule-classes :rewrite)

Theorem: len-of-atc-make-mv-nth-terms

(defthm len-of-atc-make-mv-nth-terms
  (b* ((?terms (atc-make-mv-nth-terms indices term)))
    (equal (len terms) (len indices))))