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