		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscope-subscope

Signature
(vl-elabscope-subscope key x) → subscope
Arguments: key — Guard (vl-elabkey-p key).; x — Guard (vl-elabscope-p x).
Returns: subscope — Type (iff (vl-elabscope-p subscope) subscope).

Definitions and Theorems

Function: vl-elabscope-subscope

(defun vl-elabscope-subscope (key x)
  (declare (xargs :guard (and (vl-elabkey-p key)
                              (vl-elabscope-p x))))
  (let ((__function__ 'vl-elabscope-subscope))
    (declare (ignorable __function__))
    (cdr (hons-get (vl-elabkey-fix key)
                   (vl-elabscope->subscopes x)))))

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

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

Theorem: vl-elabscope-subscope-of-vl-elabkey-fix-key

(defthm vl-elabscope-subscope-of-vl-elabkey-fix-key
  (equal (vl-elabscope-subscope (vl-elabkey-fix key)
                                x)
         (vl-elabscope-subscope key x)))

Theorem: vl-elabscope-subscope-vl-elabkey-equiv-congruence-on-key

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

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

(defthm vl-elabscope-subscope-of-vl-elabscope-fix-x
  (equal (vl-elabscope-subscope key (vl-elabscope-fix x))
         (vl-elabscope-subscope key x)))

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

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