(atj-type-annotate-mv-nth-terms types indices wrapped-mv) → terms
Function:
(defun atj-type-annotate-mv-nth-terms (types indices wrapped-mv) (declare (xargs :guard (and (atj-type-listp types) (nat-listp indices) (pseudo-termp wrapped-mv)))) (declare (xargs :guard (= (len types) (len indices)))) (let ((__function__ 'atj-type-annotate-mv-nth-terms)) (declare (ignorable __function__)) (b* (((when (endp types)) nil) (wrapped-index (atj-type-wrap-term (pseudo-term-quote (car indices)) (list (atj-type-acl2 (atj-atype-integer))) (list (atj-type-acl2 (atj-atype-integer))))) (mv-nth-call (pseudo-term-call 'mv-nth (list wrapped-index wrapped-mv))) (wrapped-mv-nth-call (atj-type-wrap-term mv-nth-call (list (atj-type-acl2 (atj-atype-value))) (list (car types)))) (rest (atj-type-annotate-mv-nth-terms (cdr types) (cdr indices) wrapped-mv))) (cons wrapped-mv-nth-call rest))))
Theorem:
(defthm pseudo-term-listp-of-atj-type-annotate-mv-nth-terms (b* ((terms (atj-type-annotate-mv-nth-terms types indices wrapped-mv))) (pseudo-term-listp terms)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-type-annotate-mv-nth-terms (b* ((?terms (atj-type-annotate-mv-nth-terms types indices wrapped-mv))) (equal (len terms) (len types))))