(vl-revive-invalid-warning name warning) → new-warning
Function:
(defun vl-revive-invalid-warning (name warning) (declare (xargs :guard (and (stringp name) (vl-warning-p warning)))) (let ((__function__ 'vl-revive-invalid-warning)) (declare (ignorable __function__)) (b* (((vl-warning warning))) (change-vl-warning warning :msg (cat "In " name " -- " warning.msg)))))
Theorem:
(defthm vl-warning-p-of-vl-revive-invalid-warning (b* ((new-warning (vl-revive-invalid-warning name warning))) (vl-warning-p new-warning)) :rule-classes :rewrite)
Theorem:
(defthm vl-revive-invalid-warning-of-str-fix-name (equal (vl-revive-invalid-warning (str-fix name) warning) (vl-revive-invalid-warning name warning)))
Theorem:
(defthm vl-revive-invalid-warning-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-revive-invalid-warning name warning) (vl-revive-invalid-warning name-equiv warning))) :rule-classes :congruence)
Theorem:
(defthm vl-revive-invalid-warning-of-vl-warning-fix-warning (equal (vl-revive-invalid-warning name (vl-warning-fix warning)) (vl-revive-invalid-warning name warning)))
Theorem:
(defthm vl-revive-invalid-warning-vl-warning-equiv-congruence-on-warning (implies (vl-warning-equiv warning warning-equiv) (equal (vl-revive-invalid-warning name warning) (vl-revive-invalid-warning name warning-equiv))) :rule-classes :congruence)