		Search-engine friendly clone of the ACL2 documentation.

Vl-loadstate

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 (and (vl-loadstate-p new-st) (equal (vl-loadstate->descs new-st) (vl-loadstate->descs 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* ((w (make-vl-warning :type type
                             :msg msg
                             :args args
                             :fn fn
                             :fatalp fatalp))
         (warnings (vl-loadstate->warnings st)))
      (vl-loadstate-set-warnings (cons w warnings)))))

Theorem: return-type-of-vl-loadstate-warn

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