(check-type-list types ctxt) → yes/no
Function:
(defun check-type-list (types ctxt) (declare (xargs :guard (and (type-listp types) (contextp ctxt)))) (let ((__function__ 'check-type-list)) (declare (ignorable __function__)) (or (endp types) (and (check-type (car types) ctxt) (check-type-list (cdr types) ctxt)))))
Theorem:
(defthm booleanp-of-check-type-list (b* ((yes/no (check-type-list types ctxt))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm check-type-list-of-type-list-fix-types (equal (check-type-list (type-list-fix types) ctxt) (check-type-list types ctxt)))
Theorem:
(defthm check-type-list-type-list-equiv-congruence-on-types (implies (type-list-equiv types types-equiv) (equal (check-type-list types ctxt) (check-type-list types-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-type-list-of-context-fix-ctxt (equal (check-type-list types (context-fix ctxt)) (check-type-list types ctxt)))
Theorem:
(defthm check-type-list-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-type-list types ctxt) (check-type-list types ctxt-equiv))) :rule-classes :congruence)