(vl-assignpat-cast-type-error-warn type-err x ss) → warnings
Function:
(defun vl-assignpat-cast-type-error-warn (type-err x ss) (declare (xargs :guard (and (vl-maybe-type-error-p type-err) (vl-expr-p x) (vl-scopestack-p ss)))) (declare (xargs :guard (vl-expr-case x :vl-pattern x.pattype :otherwise nil))) (let ((__function__ 'vl-assignpat-cast-type-error-warn)) (declare (ignorable __function__)) (b* (((unless type-err) nil) ((vl-pattern x))) (vl-type-error-basic-warn (change-vl-pattern x :pattype nil) nil type-err nil x.pattype ss))))
Theorem:
(defthm vl-warninglist-p-of-vl-assignpat-cast-type-error-warn (b* ((warnings (vl-assignpat-cast-type-error-warn type-err x ss))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignpat-cast-type-error-warn-of-vl-maybe-type-error-fix-type-err (equal (vl-assignpat-cast-type-error-warn (vl-maybe-type-error-fix type-err) x ss) (vl-assignpat-cast-type-error-warn type-err x ss)))
Theorem:
(defthm vl-assignpat-cast-type-error-warn-vl-maybe-type-error-equiv-congruence-on-type-err (implies (vl-maybe-type-error-equiv type-err type-err-equiv) (equal (vl-assignpat-cast-type-error-warn type-err x ss) (vl-assignpat-cast-type-error-warn type-err-equiv x ss))) :rule-classes :congruence)
Theorem:
(defthm vl-assignpat-cast-type-error-warn-of-vl-expr-fix-x (equal (vl-assignpat-cast-type-error-warn type-err (vl-expr-fix x) ss) (vl-assignpat-cast-type-error-warn type-err x ss)))
Theorem:
(defthm vl-assignpat-cast-type-error-warn-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-assignpat-cast-type-error-warn type-err x ss) (vl-assignpat-cast-type-error-warn type-err x-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-assignpat-cast-type-error-warn-of-vl-scopestack-fix-ss (equal (vl-assignpat-cast-type-error-warn type-err x (vl-scopestack-fix ss)) (vl-assignpat-cast-type-error-warn type-err x ss)))
Theorem:
(defthm vl-assignpat-cast-type-error-warn-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-assignpat-cast-type-error-warn type-err x ss) (vl-assignpat-cast-type-error-warn type-err x ss-equiv))) :rule-classes :congruence)