		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)