Lift atj-adapt-expr-to-type to lists.
(atj-adapt-exprs-to-types exprs src-types dst-types guards$) → new-exprs
This is used for all the arguments of a function call.
Function:
(defun atj-adapt-exprs-to-types (exprs src-types dst-types guards$) (declare (xargs :guard (and (jexpr-listp exprs) (atj-type-listp src-types) (atj-type-listp dst-types) (booleanp guards$)))) (declare (xargs :guard (and (= (len exprs) (len src-types)) (= (len exprs) (len dst-types))))) (let ((__function__ 'atj-adapt-exprs-to-types)) (declare (ignorable __function__)) (cond ((endp exprs) nil) (t (cons (atj-adapt-expr-to-type (car exprs) (car src-types) (car dst-types) guards$) (atj-adapt-exprs-to-types (cdr exprs) (cdr src-types) (cdr dst-types) guards$))))))
Theorem:
(defthm jexpr-listp-of-atj-adapt-exprs-to-types (b* ((new-exprs (atj-adapt-exprs-to-types exprs src-types dst-types guards$))) (jexpr-listp new-exprs)) :rule-classes :rewrite)