		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabindex->undostack

Signature
(vl-elabindex->undostack &optional (elabindex 'elabindex)) → undostack
Returns: undostack — Type (vl-elabtraversal-stack-p undostack).

Definitions and Theorems

Function: vl-elabindex->undostack-fn

(defun vl-elabindex->undostack-fn (elabindex)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-elabindex->undostack))
    (declare (ignorable __function__))
    (vl-elabtraversal-stack-fix
         (vl-elabindex->undostack1 elabindex))))

Theorem: vl-elabtraversal-stack-p-of-vl-elabindex->undostack

(defthm vl-elabtraversal-stack-p-of-vl-elabindex->undostack
  (b* ((undostack (vl-elabindex->undostack-fn elabindex)))
    (vl-elabtraversal-stack-p undostack))
  :rule-classes :rewrite)