		Search-engine friendly clone of the ACL2 documentation.

Vl-loadstate-p

Vl-loadstate-warn

Signature
(vl-loadstate-warn &key type msg args (fn '__function__) fatalp (st 'st)) → new-st
Arguments: type — Guard (symbolp type).; msg — Guard (stringp msg).; args — Guard (true-listp args).; fn — Guard (symbolp fn).; fatalp — Guard (booleanp fatalp).; st — Guard (vl-loadstate-p st).
Returns: new-st — Type (vl-loadstate-p new-st).

Definitions and Theorems

Function: vl-loadstate-warn-fn

(defun vl-loadstate-warn-fn (type msg args fn fatalp st)
 (declare (xargs :guard (and (symbolp type)
                             (stringp msg)
                             (true-listp args)
                             (symbolp fn)
                             (booleanp fatalp)
                             (vl-loadstate-p st))))
 (let ((__function__ 'vl-loadstate-warn))
  (declare (ignorable __function__))
  (b*
   (((vl-loadstate st) st)
    ((vl-parsestate st.pstate) st.pstate)
    (w (make-vl-warning :type type
                        :msg msg
                        :args args
                        :fn fn
                        :fatalp fatalp))
    (new-pstate
      (change-vl-parsestate st.pstate
                            :warnings (cons w st.pstate.warnings))))
   (change-vl-loadstate st
                        :pstate new-pstate))))

Theorem: vl-loadstate-p-of-vl-loadstate-warn

(defthm vl-loadstate-p-of-vl-loadstate-warn
  (b* ((new-st (vl-loadstate-warn-fn type msg args fn fatalp st)))
    (vl-loadstate-p new-st))
  :rule-classes :rewrite)