		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-init-ss

Makes an empty elabscopes at the same nesting depth as the given scopestack.

Signature
(vl-elabscopes-init-ss ss) → init-scopes
Arguments: ss — Guard (vl-scopestack-p ss).
Returns: init-scopes — Type (vl-elabscopes-p init-scopes).

Definitions and Theorems

Function: vl-elabscopes-init-ss

(defun vl-elabscopes-init-ss (ss)
  (declare (xargs :guard (vl-scopestack-p ss)))
  (let ((__function__ 'vl-elabscopes-init-ss))
    (declare (ignorable __function__))
    (make-list (vl-scopestack-nesting-level ss)
               :initial-element (cons nil (make-vl-elabscope)))))

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

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

Theorem: vl-elabscopes-init-ss-of-vl-scopestack-fix-ss

(defthm vl-elabscopes-init-ss-of-vl-scopestack-fix-ss
  (equal (vl-elabscopes-init-ss (vl-scopestack-fix ss))
         (vl-elabscopes-init-ss ss)))

Theorem: vl-elabscopes-init-ss-vl-scopestack-equiv-congruence-on-ss

(defthm vl-elabscopes-init-ss-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-elabscopes-init-ss ss)
                  (vl-elabscopes-init-ss ss-equiv)))
  :rule-classes :congruence)