		Search-engine friendly clone of the ACL2 documentation.

Vl-loadstate

Vl-loadstate-fatal

Signature
(vl-loadstate-fatal &key type msg args (fn '__function__) st) → new-st
Arguments: type — Guard (symbolp type).; msg — Guard (stringp msg).; args — Guard (true-listp args).; fn — Guard (symbolp fn).; 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-fatal-fn

(defun vl-loadstate-fatal-fn (type msg args fn st)
  (declare (xargs :guard (and (symbolp type)
                              (stringp msg)
                              (true-listp args)
                              (symbolp fn)
                              (vl-loadstate-p st))))
  (let ((__function__ 'vl-loadstate-fatal))
    (declare (ignorable __function__))
    (b* ((w (make-vl-warning :fatalp t
                             :type type
                             :msg msg
                             :args args
                             :fn fn))
         (warnings (vl-loadstate->warnings st))
         (st (vl-loadstate-set-warnings (cons w warnings)))
         (wstr (with-local-ps (vl-print-warning w)))
         (padded (str::prefix-lines wstr (vl-loadstate-pad st))))
      (cw-unformatted padded)
      st)))

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

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