		Search-engine friendly clone of the ACL2 documentation.

Vl-expr

Vl-expr-update-atts

Change the attributes of any expression.

Signature
(vl-expr-update-atts x atts) → new-x
Arguments: x — Expression to modify.
Guard (vl-expr-p x).; atts — New attributes to install. Any previous attributes will be overwritten.
Guard (vl-atts-p atts).
Returns: new-x — Type (vl-expr-p new-x).

Definitions and Theorems

Function: vl-expr-update-atts

(defun vl-expr-update-atts (x atts)
 (declare (xargs :guard (and (vl-expr-p x) (vl-atts-p atts))))
 (let ((__function__ 'vl-expr-update-atts))
   (declare (ignorable __function__))
   (vl-expr-case
        x
        :vl-special (change-vl-special x :atts atts)
        :vl-literal (change-vl-literal x :atts atts)
        :vl-index (change-vl-index x :atts atts)
        :vl-unary (change-vl-unary x :atts atts)
        :vl-binary (change-vl-binary x :atts atts)
        :vl-qmark (change-vl-qmark x :atts atts)
        :vl-mintypmax (change-vl-mintypmax x :atts atts)
        :vl-concat (change-vl-concat x :atts atts)
        :vl-multiconcat (change-vl-multiconcat x :atts atts)
        :vl-bitselect-expr (change-vl-bitselect-expr x :atts atts)
        :vl-partselect-expr (change-vl-partselect-expr x :atts atts)
        :vl-stream (change-vl-stream x :atts atts)
        :vl-call (change-vl-call x :atts atts)
        :vl-cast (change-vl-cast x :atts atts)
        :vl-inside (change-vl-inside x :atts atts)
        :vl-tagged (change-vl-tagged x :atts atts)
        :vl-pattern (change-vl-pattern x :atts atts)
        :vl-eventexpr (change-vl-eventexpr x :atts atts))))

Theorem: vl-expr-p-of-vl-expr-update-atts

(defthm vl-expr-p-of-vl-expr-update-atts
  (b* ((new-x (vl-expr-update-atts x atts)))
    (vl-expr-p new-x))
  :rule-classes :rewrite)

Theorem: vl-expr->atts-of-vl-expr-update-atts

(defthm vl-expr->atts-of-vl-expr-update-atts
  (b* ((?new-x (vl-expr-update-atts x atts)))
    (equal (vl-expr->atts new-x)
           (vl-atts-fix atts))))

Theorem: vl-expr-kind-of-vl-expr-update-atts

(defthm vl-expr-kind-of-vl-expr-update-atts
  (b* ((?new-x (vl-expr-update-atts x atts)))
    (equal (vl-expr-kind new-x)
           (vl-expr-kind x))))

Theorem: vl-expr-update-atts-of-vl-expr-fix-x

(defthm vl-expr-update-atts-of-vl-expr-fix-x
  (equal (vl-expr-update-atts (vl-expr-fix x)
                              atts)
         (vl-expr-update-atts x atts)))

Theorem: vl-expr-update-atts-vl-expr-equiv-congruence-on-x

(defthm vl-expr-update-atts-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-expr-update-atts x atts)
                  (vl-expr-update-atts x-equiv atts)))
  :rule-classes :congruence)

Theorem: vl-expr-update-atts-of-vl-atts-fix-atts

(defthm vl-expr-update-atts-of-vl-atts-fix-atts
  (equal (vl-expr-update-atts x (vl-atts-fix atts))
         (vl-expr-update-atts x atts)))

Theorem: vl-expr-update-atts-vl-atts-equiv-congruence-on-atts

(defthm vl-expr-update-atts-vl-atts-equiv-congruence-on-atts
  (implies (vl-atts-equiv atts atts-equiv)
           (equal (vl-expr-update-atts x atts)
                  (vl-expr-update-atts x atts-equiv)))
  :rule-classes :congruence)