Get the warning field from a vl-warningtree-warning.
(vl-warningtree->warning x) → warning
This is an ordinary field accessor created by defprod.
Function:
(defun vl-warningtree->warning$inline (x) (declare (xargs :guard (vl-warningtree-p x))) (declare (xargs :guard (equal (vl-warningtree-kind x) :warning))) (let ((__function__ 'vl-warningtree->warning)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and (equal (vl-warningtree-kind x) :warning) x))) (vl-warning-fix x)) :exec x)))
Theorem:
(defthm vl-warning-p-of-vl-warningtree->warning (b* ((warning (vl-warningtree->warning$inline x))) (vl-warning-p warning)) :rule-classes :rewrite)
Theorem:
(defthm vl-warningtree->warning$inline-of-vl-warningtree-fix-x (equal (vl-warningtree->warning$inline (vl-warningtree-fix x)) (vl-warningtree->warning$inline x)))
Theorem:
(defthm vl-warningtree->warning$inline-vl-warningtree-equiv-congruence-on-x (implies (vl-warningtree-equiv x x-equiv) (equal (vl-warningtree->warning$inline x) (vl-warningtree->warning$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-warningtree->warning-when-wrong-kind (implies (not (equal (vl-warningtree-kind x) :warning)) (equal (vl-warningtree->warning x) (vl-warning-fix nil))))