		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscope-package-subscope

Signature
(vl-elabscope-package-subscope name x) → subscope
Arguments: name — Guard (stringp name).; x — Guard (vl-elabscope-p x).
Returns: subscope — Type (iff (vl-elabscope-p subscope) subscope).

Definitions and Theorems

Function: vl-elabscope-package-subscope

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

Theorem: return-type-of-vl-elabscope-package-subscope

(defthm return-type-of-vl-elabscope-package-subscope
  (b* ((subscope (vl-elabscope-package-subscope name x)))
    (iff (vl-elabscope-p subscope)
         subscope))
  :rule-classes :rewrite)

Theorem: vl-elabscope-package-subscope-of-str-fix-name

(defthm vl-elabscope-package-subscope-of-str-fix-name
  (equal (vl-elabscope-package-subscope (str-fix name)
                                        x)
         (vl-elabscope-package-subscope name x)))

Theorem: vl-elabscope-package-subscope-streqv-congruence-on-name

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

Theorem: vl-elabscope-package-subscope-of-vl-elabscope-fix-x

(defthm vl-elabscope-package-subscope-of-vl-elabscope-fix-x
  (equal (vl-elabscope-package-subscope name (vl-elabscope-fix x))
         (vl-elabscope-package-subscope name x)))

Theorem: vl-elabscope-package-subscope-vl-elabscope-equiv-congruence-on-x

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