		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabindex->ss

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

Definitions and Theorems

Function: vl-elabindex->ss-fn

(defun vl-elabindex->ss-fn (elabindex)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-elabindex->ss))
    (declare (ignorable __function__))
    (vl-scopestack-fix (vl-elabindex->ss1 elabindex))))

Theorem: vl-scopestack-p-of-vl-elabindex->ss

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