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