		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabindex-push-undo-entry

Signature
(vl-elabindex-push-undo-entry &key (elabindex 'elabindex)) → undo-entry
Returns: undo-entry — Type (and (vl-elabtraversal-p (car undo-entry)) (vl-scopestack-p (cdr undo-entry))) .

Definitions and Theorems

Function: vl-elabindex-push-undo-entry-fn

(defun vl-elabindex-push-undo-entry-fn (elabindex)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-elabindex-push-undo-entry))
    (declare (ignorable __function__))
    (cons (list (vl-elabinstruction-pop 1))
          (vl-elabindex->ss))))

Theorem: return-type-of-vl-elabindex-push-undo-entry

(defthm return-type-of-vl-elabindex-push-undo-entry
  (b* ((undo-entry (vl-elabindex-push-undo-entry-fn elabindex)))
    (and (vl-elabtraversal-p (car undo-entry))
         (vl-scopestack-p (cdr undo-entry))))
  :rule-classes :rewrite)

Theorem: undostack-of-vl-elabindex-push

(defthm undostack-of-vl-elabindex-push
  (equal (vl-elabindex->undostack (vl-elabindex-push scope))
         (cons (vl-elabindex-push-undo-entry)
               (vl-elabindex->undostack))))