		Search-engine friendly clone of the ACL2 documentation.

Warnings

Vl-warning-add-ctx

Signature
(vl-warning-add-ctx x ctx) → new-x
Arguments: x — Guard (vl-warning-p x).
Returns: new-x — Type (vl-warning-p new-x).

Definitions and Theorems

Function: vl-warning-add-ctx

(defun vl-warning-add-ctx (x ctx)
  (declare (xargs :guard (vl-warning-p x)))
  (let ((__function__ 'vl-warning-add-ctx))
    (declare (ignorable __function__))
    (b* (((vl-warning x))
         ((when x.context) (vl-warning-fix x)))
      (change-vl-warning x :context ctx))))

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

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

Theorem: vl-warning-add-ctx-of-vl-warning-fix-x

(defthm vl-warning-add-ctx-of-vl-warning-fix-x
  (equal (vl-warning-add-ctx (vl-warning-fix x)
                             ctx)
         (vl-warning-add-ctx x ctx)))

Theorem: vl-warning-add-ctx-vl-warning-equiv-congruence-on-x

(defthm vl-warning-add-ctx-vl-warning-equiv-congruence-on-x
  (implies (vl-warning-equiv x x-equiv)
           (equal (vl-warning-add-ctx x ctx)
                  (vl-warning-add-ctx x-equiv ctx)))
  :rule-classes :congruence)