		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)