		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabindex->scopes

Signature
(vl-elabindex->scopes &optional (elabindex 'elabindex)) → scopes
Returns: scopes — Type (vl-elabscopes-p scopes).

Definitions and Theorems

Function: vl-elabindex->scopes-fn

(defun vl-elabindex->scopes-fn (elabindex)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-elabindex->scopes))
    (declare (ignorable __function__))
    (vl-elabscopes-fix (vl-elabindex->scopes1 elabindex))))

Theorem: vl-elabscopes-p-of-vl-elabindex->scopes

(defthm vl-elabscopes-p-of-vl-elabindex->scopes
  (b* ((scopes (vl-elabindex->scopes-fn elabindex)))
    (vl-elabscopes-p scopes))
  :rule-classes :rewrite)