		Search-engine friendly clone of the ACL2 documentation.

Vl-loadstate-p

Vl-loadstate-set-warnings

Signature
(vl-loadstate-set-warnings warnings &key (st 'st)) → new-st
Arguments: warnings — Guard (vl-warninglist-p warnings).; st — Guard (vl-loadstate-p st).
Returns: new-st — Type (vl-loadstate-p new-st).

Definitions and Theorems

Function: vl-loadstate-set-warnings-fn

(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* (((vl-loadstate st) st)
         (new-pstate (change-vl-parsestate st.pstate
                                           :warnings warnings)))
      (change-vl-loadstate st
                           :pstate new-pstate))))

Theorem: vl-loadstate-p-of-vl-loadstate-set-warnings

(defthm vl-loadstate-p-of-vl-loadstate-set-warnings
  (b* ((new-st (vl-loadstate-set-warnings-fn warnings st)))
    (vl-loadstate-p new-st))
  :rule-classes :rewrite)