		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-scope->elabkey

Signature
(vl-scope->elabkey scope) → key
Arguments: scope — Guard (vl-scope-p scope).
Returns: key — Type (and (iff (vl-elabkey-p key) key) (vl-maybe-elabkey-p key)).

Definitions and Theorems

Function: vl-scope->elabkey

(defun vl-scope->elabkey (scope)
  (declare (xargs :guard (vl-scope-p scope)))
  (let ((__function__ 'vl-scope->elabkey))
    (declare (ignorable __function__))
    (b* ((name (vl-scope->id scope))
         (type (vl-scope->scopetype scope)))
      (case type
            ((:vl-module :vl-interface)
             (and (stringp name)
                  (vl-elabkey-def name)))
            ((:vl-fundecl :vl-taskdecl :vl-genblock)
             (cond ((stringp name) (vl-elabkey-item name))
                   ((integerp name)
                    (vl-elabkey-index name))))
            ((:vl-genarray :vl-genloop)
             (and (stringp name)
                  (vl-elabkey-item name)))
            (:vl-genarrayblock (and (integerp name)
                                    (vl-elabkey-index name)))
            (:vl-package (and (stringp name)
                              (vl-elabkey-package name)))
            (:vl-class (and (stringp name)
                            (vl-elabkey-class name)))
            (otherwise nil)))))

Theorem: return-type-of-vl-scope->elabkey

(defthm return-type-of-vl-scope->elabkey
  (b* ((key (vl-scope->elabkey scope)))
    (and (iff (vl-elabkey-p key) key)
         (vl-maybe-elabkey-p key)))
  :rule-classes :rewrite)

Theorem: vl-scope->elabkey-of-vl-scope-fix-scope

(defthm vl-scope->elabkey-of-vl-scope-fix-scope
  (equal (vl-scope->elabkey (vl-scope-fix scope))
         (vl-scope->elabkey scope)))

Theorem: vl-scope->elabkey-vl-scope-equiv-congruence-on-scope

(defthm vl-scope->elabkey-vl-scope-equiv-congruence-on-scope
  (implies (vl-scope-equiv scope scope-equiv)
           (equal (vl-scope->elabkey scope)
                  (vl-scope->elabkey scope-equiv)))
  :rule-classes :congruence)