(vl-parsestate-set-warnings warnings pstate) → new-pstate
Function:
(defun vl-parsestate-set-warnings (warnings pstate) (declare (xargs :guard (and (vl-warninglist-p warnings) (vl-parsestate-p pstate)))) (let ((__function__ 'vl-parsestate-set-warnings)) (declare (ignorable __function__)) (change-vl-parsestate pstate :warnings warnings)))
Theorem:
(defthm vl-parsestate-p-of-vl-parsestate-set-warnings (b* ((new-pstate (vl-parsestate-set-warnings warnings pstate))) (vl-parsestate-p new-pstate)) :rule-classes :rewrite)