		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-expr-add-atts

Signature
(vl-expr-add-atts new-atts x) → new-x
Arguments: new-atts — Guard (vl-atts-p new-atts).; x — Guard (vl-expr-p x).
Returns: new-x — Type (vl-expr-p new-x).

Definitions and Theorems

Function: vl-expr-add-atts

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

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

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

Theorem: vl-expr-add-atts-of-vl-atts-fix-new-atts

(defthm vl-expr-add-atts-of-vl-atts-fix-new-atts
  (equal (vl-expr-add-atts (vl-atts-fix new-atts)
                           x)
         (vl-expr-add-atts new-atts x)))

Theorem: vl-expr-add-atts-vl-atts-equiv-congruence-on-new-atts

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

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

(defthm vl-expr-add-atts-of-vl-expr-fix-x
  (equal (vl-expr-add-atts new-atts (vl-expr-fix x))
         (vl-expr-add-atts new-atts x)))

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

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