(vl-type-error-qmark-combine x type-err1 type-err2) → type-err
Function:
(defun vl-type-error-qmark-combine (x type-err1 type-err2) (declare (xargs :guard (and (vl-expr-p x) (vl-maybe-type-error-p type-err1) (vl-maybe-type-error-p type-err2)))) (declare (xargs :guard (vl-expr-case x :vl-qmark))) (let ((__function__ 'vl-type-error-qmark-combine)) (declare (ignorable __function__)) (b* (((when (and (not type-err1) (not type-err2))) nil) ((when (and (not type-err1) (vl-type-error-case type-err2 :qmark-subexpr))) (vl-type-error-fix type-err2)) ((when (and (not type-err2) (vl-type-error-case type-err1 :qmark-subexpr))) (vl-type-error-fix type-err1)) ((vl-qmark x)) (alist1 (and type-err1 (vl-type-error-case type-err1 :qmark-subexpr type-err1.alist :otherwise (list (cons x.then type-err1))))) (alist2 (and type-err2 (vl-type-error-case type-err2 :qmark-subexpr type-err2.alist :otherwise (list (cons x.else type-err2)))))) (make-vl-type-error-qmark-subexpr :alist (append-without-guard alist1 alist2)))))
Theorem:
(defthm vl-maybe-type-error-p-of-vl-type-error-qmark-combine (b* ((type-err (vl-type-error-qmark-combine x type-err1 type-err2))) (vl-maybe-type-error-p type-err)) :rule-classes :rewrite)
Theorem:
(defthm vl-type-error-qmark-combine-of-vl-expr-fix-x (equal (vl-type-error-qmark-combine (vl-expr-fix x) type-err1 type-err2) (vl-type-error-qmark-combine x type-err1 type-err2)))
Theorem:
(defthm vl-type-error-qmark-combine-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-type-error-qmark-combine x type-err1 type-err2) (vl-type-error-qmark-combine x-equiv type-err1 type-err2))) :rule-classes :congruence)
Theorem:
(defthm vl-type-error-qmark-combine-of-vl-maybe-type-error-fix-type-err1 (equal (vl-type-error-qmark-combine x (vl-maybe-type-error-fix type-err1) type-err2) (vl-type-error-qmark-combine x type-err1 type-err2)))
Theorem:
(defthm vl-type-error-qmark-combine-vl-maybe-type-error-equiv-congruence-on-type-err1 (implies (vl-maybe-type-error-equiv type-err1 type-err1-equiv) (equal (vl-type-error-qmark-combine x type-err1 type-err2) (vl-type-error-qmark-combine x type-err1-equiv type-err2))) :rule-classes :congruence)
Theorem:
(defthm vl-type-error-qmark-combine-of-vl-maybe-type-error-fix-type-err2 (equal (vl-type-error-qmark-combine x type-err1 (vl-maybe-type-error-fix type-err2)) (vl-type-error-qmark-combine x type-err1 type-err2)))
Theorem:
(defthm vl-type-error-qmark-combine-vl-maybe-type-error-equiv-congruence-on-type-err2 (implies (vl-maybe-type-error-equiv type-err2 type-err2-equiv) (equal (vl-type-error-qmark-combine x type-err1 type-err2) (vl-type-error-qmark-combine x type-err1 type-err2-equiv))) :rule-classes :congruence)