		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscope-update-def-subscope

Signature
(vl-elabscope-update-def-subscope name val x) → new-x
Arguments: name — Guard (stringp name).; val — Guard (vl-elabscope-p val).; x — Guard (vl-elabscope-p x).
Returns: new-x — Type (vl-elabscope-p new-x).

Definitions and Theorems

Function: vl-elabscope-update-def-subscope

(defun vl-elabscope-update-def-subscope (name val x)
  (declare (xargs :guard (and (stringp name)
                              (vl-elabscope-p val)
                              (vl-elabscope-p x))))
  (let ((__function__ 'vl-elabscope-update-def-subscope))
    (declare (ignorable __function__))
    (vl-elabscope-update-subscope (vl-elabkey-def name)
                                  val x)))

Theorem: vl-elabscope-p-of-vl-elabscope-update-def-subscope

(defthm vl-elabscope-p-of-vl-elabscope-update-def-subscope
  (b* ((new-x (vl-elabscope-update-def-subscope name val x)))
    (vl-elabscope-p new-x))
  :rule-classes :rewrite)

Theorem: vl-elabscope-update-def-subscope-of-str-fix-name

(defthm vl-elabscope-update-def-subscope-of-str-fix-name
  (equal (vl-elabscope-update-def-subscope (str-fix name)
                                           val x)
         (vl-elabscope-update-def-subscope name val x)))

Theorem: vl-elabscope-update-def-subscope-streqv-congruence-on-name

(defthm vl-elabscope-update-def-subscope-streqv-congruence-on-name
  (implies
       (streqv name name-equiv)
       (equal (vl-elabscope-update-def-subscope name val x)
              (vl-elabscope-update-def-subscope name-equiv val x)))
  :rule-classes :congruence)

Theorem: vl-elabscope-update-def-subscope-of-vl-elabscope-fix-val

(defthm vl-elabscope-update-def-subscope-of-vl-elabscope-fix-val
  (equal
       (vl-elabscope-update-def-subscope name (vl-elabscope-fix val)
                                         x)
       (vl-elabscope-update-def-subscope name val x)))

Theorem: vl-elabscope-update-def-subscope-vl-elabscope-equiv-congruence-on-val

(defthm
 vl-elabscope-update-def-subscope-vl-elabscope-equiv-congruence-on-val
 (implies
      (vl-elabscope-equiv val val-equiv)
      (equal (vl-elabscope-update-def-subscope name val x)
             (vl-elabscope-update-def-subscope name val-equiv x)))
 :rule-classes :congruence)

Theorem: vl-elabscope-update-def-subscope-of-vl-elabscope-fix-x

(defthm vl-elabscope-update-def-subscope-of-vl-elabscope-fix-x
 (equal
    (vl-elabscope-update-def-subscope name val (vl-elabscope-fix x))
    (vl-elabscope-update-def-subscope name val x)))

Theorem: vl-elabscope-update-def-subscope-vl-elabscope-equiv-congruence-on-x

(defthm
 vl-elabscope-update-def-subscope-vl-elabscope-equiv-congruence-on-x
 (implies
      (vl-elabscope-equiv x x-equiv)
      (equal (vl-elabscope-update-def-subscope name val x)
             (vl-elabscope-update-def-subscope name val x-equiv)))
 :rule-classes :congruence)