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