(vl-loadstate-set-warnings warnings &key (st 'st)) → new-st
Function:
(defun vl-loadstate-set-warnings-fn (warnings st) (declare (xargs :guard (and (vl-warninglist-p warnings) (vl-loadstate-p st)))) (let ((__function__ 'vl-loadstate-set-warnings)) (declare (ignorable __function__)) (b* ((?pstate (vl-loadstate->pstate st)) (new-pstate (change-vl-parsestate pstate :warnings warnings))) (change-vl-loadstate st :pstate new-pstate))))
Theorem:
(defthm return-type-of-vl-loadstate-set-warnings (b* ((new-st (vl-loadstate-set-warnings-fn warnings st))) (and (vl-loadstate-p new-st) (equal (vl-loadstate->descs new-st) (vl-loadstate->descs st)))) :rule-classes :rewrite)