		Search-engine friendly clone of the ACL2 documentation.

Vl-parsestate

Vl-parsestate-add-warning

Extend the parse state with a new warning.

Signature
(vl-parsestate-add-warning warning pstate) → new-pstate
Arguments: warning — Guard (vl-warning-p warning).; pstate — Guard (vl-parsestate-p pstate).
Returns: new-pstate — Type (vl-parsestate-p new-pstate).

Definitions and Theorems

Function: vl-parsestate-add-warning

(defun vl-parsestate-add-warning (warning pstate)
  (declare (xargs :guard (and (vl-warning-p warning)
                              (vl-parsestate-p pstate))))
  (let ((__function__ 'vl-parsestate-add-warning))
    (declare (ignorable __function__))
    (b* (((vl-parsestate pstate) pstate))
      (change-vl-parsestate
           pstate
           :warnings (cons warning pstate.warnings)))))

Theorem: vl-parsestate-p-of-vl-parsestate-add-warning

(defthm vl-parsestate-p-of-vl-parsestate-add-warning
  (b* ((new-pstate (vl-parsestate-add-warning warning pstate)))
    (vl-parsestate-p new-pstate))
  :rule-classes :rewrite)