(vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss) → warnings
Function:
(defun vl-struct-assignpat-keyval-type-err-warn (x structmem subexpr type-err ss) (declare (xargs :guard (and (vl-expr-p x) (vl-structmember-p structmem) (vl-expr-p subexpr) (vl-maybe-type-error-p type-err) (vl-scopestack-p ss)))) (let ((__function__ 'vl-struct-assignpat-keyval-type-err-warn)) (declare (ignorable __function__)) (b* (((unless type-err) nil) ((vl-structmember structmem))) (vl-type-error-basic-warn x (vl-expr-fix subexpr) type-err (vl-idexpr structmem.name) structmem.type ss))))
Theorem:
(defthm vl-warninglist-p-of-vl-struct-assignpat-keyval-type-err-warn (b* ((warnings (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-struct-assignpat-keyval-type-err-warn-of-vl-expr-fix-x (equal (vl-struct-assignpat-keyval-type-err-warn (vl-expr-fix x) structmem subexpr type-err ss) (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss)))
Theorem:
(defthm vl-struct-assignpat-keyval-type-err-warn-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss) (vl-struct-assignpat-keyval-type-err-warn x-equiv structmem subexpr type-err ss))) :rule-classes :congruence)
Theorem:
(defthm vl-struct-assignpat-keyval-type-err-warn-of-vl-structmember-fix-structmem (equal (vl-struct-assignpat-keyval-type-err-warn x (vl-structmember-fix structmem) subexpr type-err ss) (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss)))
Theorem:
(defthm vl-struct-assignpat-keyval-type-err-warn-vl-structmember-equiv-congruence-on-structmem (implies (vl-structmember-equiv structmem structmem-equiv) (equal (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss) (vl-struct-assignpat-keyval-type-err-warn x structmem-equiv subexpr type-err ss))) :rule-classes :congruence)
Theorem:
(defthm vl-struct-assignpat-keyval-type-err-warn-of-vl-expr-fix-subexpr (equal (vl-struct-assignpat-keyval-type-err-warn x structmem (vl-expr-fix subexpr) type-err ss) (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss)))
Theorem:
(defthm vl-struct-assignpat-keyval-type-err-warn-vl-expr-equiv-congruence-on-subexpr (implies (vl-expr-equiv subexpr subexpr-equiv) (equal (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss) (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr-equiv type-err ss))) :rule-classes :congruence)
Theorem:
(defthm vl-struct-assignpat-keyval-type-err-warn-of-vl-maybe-type-error-fix-type-err (equal (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr (vl-maybe-type-error-fix type-err) ss) (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss)))
Theorem:
(defthm vl-struct-assignpat-keyval-type-err-warn-vl-maybe-type-error-equiv-congruence-on-type-err (implies (vl-maybe-type-error-equiv type-err type-err-equiv) (equal (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss) (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-struct-assignpat-keyval-type-err-warn-of-vl-scopestack-fix-ss (equal (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err (vl-scopestack-fix ss)) (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss)))
Theorem:
(defthm vl-struct-assignpat-keyval-type-err-warn-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss) (vl-struct-assignpat-keyval-type-err-warn x structmem subexpr type-err ss-equiv))) :rule-classes :congruence)