Create a list of mv-lets with the same bindings and with bodies from a list of terms, in the same order.
(atc-make-mv-lets-of-uterms vars vars-uterms uterms) → mv-let-uterms
Function:
(defun atc-make-mv-lets-of-uterms (vars vars-uterms uterms) (declare (xargs :guard (true-listp uterms))) (let ((__function__ 'atc-make-mv-lets-of-uterms)) (declare (ignorable __function__)) (cond ((endp uterms) nil) (t (cons (cons 'mv-let (cons vars (cons vars-uterms (cons (car uterms) 'nil)))) (atc-make-mv-lets-of-uterms vars vars-uterms (cdr uterms)))))))
Theorem:
(defthm true-listp-of-atc-make-mv-lets-of-uterms (b* ((mv-let-uterms (atc-make-mv-lets-of-uterms vars vars-uterms uterms))) (true-listp mv-let-uterms)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atc-make-mv-lets-of-uterms (b* ((?mv-let-uterms (atc-make-mv-lets-of-uterms vars vars-uterms uterms))) (equal (len mv-let-uterms) (len uterms))))