(vl-datatype-compatibility-type-error req-type actual-type compattype) → type-err
Function:
(defun vl-datatype-compatibility-type-error (req-type actual-type compattype) (declare (xargs :guard (and (vl-datatype-p req-type) (vl-datatype-p actual-type) (vl-typecompat-p compattype)))) (declare (xargs :guard (and (vl-datatype-resolved-p req-type) (vl-datatype-resolved-p actual-type)))) (let ((__function__ 'vl-datatype-compatibility-type-error)) (declare (ignorable __function__)) (b* ((msg (vl-check-datatype-compatibility req-type actual-type compattype))) (and msg (make-vl-type-error-incompat :actual-type actual-type :detail msg)))))
Theorem:
(defthm vl-maybe-type-error-p-of-vl-datatype-compatibility-type-error (b* ((type-err (vl-datatype-compatibility-type-error req-type actual-type compattype))) (vl-maybe-type-error-p type-err)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-compatibility-type-error-of-vl-datatype-fix-req-type (equal (vl-datatype-compatibility-type-error (vl-datatype-fix req-type) actual-type compattype) (vl-datatype-compatibility-type-error req-type actual-type compattype)))
Theorem:
(defthm vl-datatype-compatibility-type-error-vl-datatype-equiv-congruence-on-req-type (implies (vl-datatype-equiv req-type req-type-equiv) (equal (vl-datatype-compatibility-type-error req-type actual-type compattype) (vl-datatype-compatibility-type-error req-type-equiv actual-type compattype))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-compatibility-type-error-of-vl-datatype-fix-actual-type (equal (vl-datatype-compatibility-type-error req-type (vl-datatype-fix actual-type) compattype) (vl-datatype-compatibility-type-error req-type actual-type compattype)))
Theorem:
(defthm vl-datatype-compatibility-type-error-vl-datatype-equiv-congruence-on-actual-type (implies (vl-datatype-equiv actual-type actual-type-equiv) (equal (vl-datatype-compatibility-type-error req-type actual-type compattype) (vl-datatype-compatibility-type-error req-type actual-type-equiv compattype))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-compatibility-type-error-of-vl-typecompat-fix-compattype (equal (vl-datatype-compatibility-type-error req-type actual-type (vl-typecompat-fix compattype)) (vl-datatype-compatibility-type-error req-type actual-type compattype)))
Theorem:
(defthm vl-datatype-compatibility-type-error-vl-typecompat-equiv-congruence-on-compattype (implies (vl-typecompat-equiv compattype compattype-equiv) (equal (vl-datatype-compatibility-type-error req-type actual-type compattype) (vl-datatype-compatibility-type-error req-type actual-type compattype-equiv))) :rule-classes :congruence)