(vl-subexpr-type-error-list-warn x type-errs ss) → warnings
Function:
(defun vl-subexpr-type-error-list-warn (x type-errs ss) (declare (xargs :guard (and (vl-expr-p x) (vl-subexpr-type-error-list-p type-errs) (vl-scopestack-p ss)))) (let ((__function__ 'vl-subexpr-type-error-list-warn)) (declare (ignorable __function__)) (b* (((when (atom type-errs)) nil) (warnings (vl-subexpr-type-error-list-warn x (cdr type-errs) ss)) ((vl-subexpr-type-error err1) (car type-errs)) ((wmv warnings) (vl-type-error-basic-warn x err1.expr err1.type-err nil err1.type ss))) warnings)))
Theorem:
(defthm vl-warninglist-p-of-vl-subexpr-type-error-list-warn (b* ((warnings (vl-subexpr-type-error-list-warn x type-errs ss))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-subexpr-type-error-list-warn-of-vl-expr-fix-x (equal (vl-subexpr-type-error-list-warn (vl-expr-fix x) type-errs ss) (vl-subexpr-type-error-list-warn x type-errs ss)))
Theorem:
(defthm vl-subexpr-type-error-list-warn-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-subexpr-type-error-list-warn x type-errs ss) (vl-subexpr-type-error-list-warn x-equiv type-errs ss))) :rule-classes :congruence)
Theorem:
(defthm vl-subexpr-type-error-list-warn-of-vl-subexpr-type-error-list-fix-type-errs (equal (vl-subexpr-type-error-list-warn x (vl-subexpr-type-error-list-fix type-errs) ss) (vl-subexpr-type-error-list-warn x type-errs ss)))
Theorem:
(defthm vl-subexpr-type-error-list-warn-vl-subexpr-type-error-list-equiv-congruence-on-type-errs (implies (vl-subexpr-type-error-list-equiv type-errs type-errs-equiv) (equal (vl-subexpr-type-error-list-warn x type-errs ss) (vl-subexpr-type-error-list-warn x type-errs-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-subexpr-type-error-list-warn-of-vl-scopestack-fix-ss (equal (vl-subexpr-type-error-list-warn x type-errs (vl-scopestack-fix ss)) (vl-subexpr-type-error-list-warn x type-errs ss)))
Theorem:
(defthm vl-subexpr-type-error-list-warn-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-subexpr-type-error-list-warn x type-errs ss) (vl-subexpr-type-error-list-warn x type-errs ss-equiv))) :rule-classes :congruence)