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