Lift atj-type-to-jitype to lists.
(atj-type-list-to-jitype-list types) → jtypes
Function:
(defun atj-type-list-to-jitype-list (types) (declare (xargs :guard (atj-type-listp types))) (let ((__function__ 'atj-type-list-to-jitype-list)) (declare (ignorable __function__)) (cond ((endp types) nil) (t (cons (atj-type-to-jitype (car types)) (atj-type-list-to-jitype-list (cdr types)))))))
Theorem:
(defthm atj-jitype-listp-of-atj-type-list-to-jitype-list (b* ((jtypes (atj-type-list-to-jitype-list types))) (atj-jitype-listp jtypes)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-type-list-to-jitype-list (b* ((?jtypes (atj-type-list-to-jitype-list types))) (equal (len jtypes) (len types))))
Theorem:
(defthm atj-type-list-to-jitype-list-of-atj-type-list-fix-types (equal (atj-type-list-to-jitype-list (atj-type-list-fix types)) (atj-type-list-to-jitype-list types)))
Theorem:
(defthm atj-type-list-to-jitype-list-atj-type-list-equiv-congruence-on-types (implies (atj-type-list-equiv types types-equiv) (equal (atj-type-list-to-jitype-list types) (atj-type-list-to-jitype-list types-equiv))) :rule-classes :congruence)