(vl-subexpr-type-error-list-combine x type err rest) → errs
Function:
(defun vl-subexpr-type-error-list-combine (x type err rest) (declare (xargs :guard (and (vl-expr-p x) (vl-datatype-p type) (vl-maybe-type-error-p err) (vl-subexpr-type-error-list-p rest)))) (let ((__function__ 'vl-subexpr-type-error-list-combine)) (declare (ignorable __function__)) (if err (cons (make-vl-subexpr-type-error :expr x :type type :type-err err) (vl-subexpr-type-error-list-fix rest)) (vl-subexpr-type-error-list-fix rest))))
Theorem:
(defthm vl-subexpr-type-error-list-p-of-vl-subexpr-type-error-list-combine (b* ((errs (vl-subexpr-type-error-list-combine x type err rest))) (vl-subexpr-type-error-list-p errs)) :rule-classes :rewrite)
Theorem:
(defthm vl-subexpr-type-error-list-combine-of-vl-expr-fix-x (equal (vl-subexpr-type-error-list-combine (vl-expr-fix x) type err rest) (vl-subexpr-type-error-list-combine x type err rest)))
Theorem:
(defthm vl-subexpr-type-error-list-combine-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-subexpr-type-error-list-combine x type err rest) (vl-subexpr-type-error-list-combine x-equiv type err rest))) :rule-classes :congruence)
Theorem:
(defthm vl-subexpr-type-error-list-combine-of-vl-datatype-fix-type (equal (vl-subexpr-type-error-list-combine x (vl-datatype-fix type) err rest) (vl-subexpr-type-error-list-combine x type err rest)))
Theorem:
(defthm vl-subexpr-type-error-list-combine-vl-datatype-equiv-congruence-on-type (implies (vl-datatype-equiv type type-equiv) (equal (vl-subexpr-type-error-list-combine x type err rest) (vl-subexpr-type-error-list-combine x type-equiv err rest))) :rule-classes :congruence)
Theorem:
(defthm vl-subexpr-type-error-list-combine-of-vl-maybe-type-error-fix-err (equal (vl-subexpr-type-error-list-combine x type (vl-maybe-type-error-fix err) rest) (vl-subexpr-type-error-list-combine x type err rest)))
Theorem:
(defthm vl-subexpr-type-error-list-combine-vl-maybe-type-error-equiv-congruence-on-err (implies (vl-maybe-type-error-equiv err err-equiv) (equal (vl-subexpr-type-error-list-combine x type err rest) (vl-subexpr-type-error-list-combine x type err-equiv rest))) :rule-classes :congruence)
Theorem:
(defthm vl-subexpr-type-error-list-combine-of-vl-subexpr-type-error-list-fix-rest (equal (vl-subexpr-type-error-list-combine x type err (vl-subexpr-type-error-list-fix rest)) (vl-subexpr-type-error-list-combine x type err rest)))
Theorem:
(defthm vl-subexpr-type-error-list-combine-vl-subexpr-type-error-list-equiv-congruence-on-rest (implies (vl-subexpr-type-error-list-equiv rest rest-equiv) (equal (vl-subexpr-type-error-list-combine x type err rest) (vl-subexpr-type-error-list-combine x type err rest-equiv))) :rule-classes :congruence)