		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-init

Signature
(vl-elabscopes-init) → init-scopes
Returns: init-scopes — Type (vl-elabscopes-p init-scopes).

Definitions and Theorems

Function: vl-elabscopes-init

(defun vl-elabscopes-init nil
  (declare (xargs :guard t))
  (let ((__function__ 'vl-elabscopes-init))
    (declare (ignorable __function__))
    (list (cons nil (make-vl-elabscope)))))

Theorem: vl-elabscopes-p-of-vl-elabscopes-init

(defthm vl-elabscopes-p-of-vl-elabscopes-init
  (b* ((init-scopes (vl-elabscopes-init)))
    (vl-elabscopes-p init-scopes))
  :rule-classes :rewrite)