		Search-engine friendly clone of the ACL2 documentation.

Loader

Vl-loadstate->warnings

Signature
(vl-loadstate->warnings st) → warnings
Arguments: st — Guard (vl-loadstate-p st).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-loadstate->warnings

(defun vl-loadstate->warnings (st)
  (declare (xargs :guard (vl-loadstate-p st)))
  (let ((__function__ 'vl-loadstate->warnings))
    (declare (ignorable __function__))
    (vl-parsestate->warnings (vl-loadstate->pstate st))))

Theorem: vl-warninglist-p-of-vl-loadstate->warnings

(defthm vl-warninglist-p-of-vl-loadstate->warnings
  (b* ((warnings (vl-loadstate->warnings st)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)