		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-push-scope

Signature
(vl-elabscopes-push-scope x scopes &key (allow-empty 'nil)) → new-scopes
Arguments: x — Guard (vl-scope-p x).; scopes — Guard (vl-elabscopes-p scopes).
Returns: new-scopes — Type (vl-elabscopes-p new-scopes).

Definitions and Theorems

Function: vl-elabscopes-push-scope-fn

(defun vl-elabscopes-push-scope-fn (x scopes allow-empty)
  (declare (xargs :guard (and (vl-scope-p x)
                              (vl-elabscopes-p scopes))))
  (let ((__function__ 'vl-elabscopes-push-scope))
    (declare (ignorable __function__))
    (b* ((scopes (vl-elabscopes-fix scopes))
         (key (vl-scope->elabkey x))
         ((when key)
          (vl-elabscopes-push-named key scopes
                                    :allow-empty allow-empty)))
      (vl-elabscopes-push-anon (make-vl-elabscope)
                               scopes))))

Theorem: vl-elabscopes-p-of-vl-elabscopes-push-scope

(defthm vl-elabscopes-p-of-vl-elabscopes-push-scope
  (b*
   ((new-scopes (vl-elabscopes-push-scope-fn x scopes allow-empty)))
   (vl-elabscopes-p new-scopes))
  :rule-classes :rewrite)

Theorem: vl-elabscopes-push-scope-fn-of-vl-scope-fix-x

(defthm vl-elabscopes-push-scope-fn-of-vl-scope-fix-x
  (equal (vl-elabscopes-push-scope-fn (vl-scope-fix x)
                                      scopes allow-empty)
         (vl-elabscopes-push-scope-fn x scopes allow-empty)))

Theorem: vl-elabscopes-push-scope-fn-vl-scope-equiv-congruence-on-x

(defthm vl-elabscopes-push-scope-fn-vl-scope-equiv-congruence-on-x
 (implies
   (vl-scope-equiv x x-equiv)
   (equal (vl-elabscopes-push-scope-fn x scopes allow-empty)
          (vl-elabscopes-push-scope-fn x-equiv scopes allow-empty)))
 :rule-classes :congruence)

Theorem: vl-elabscopes-push-scope-fn-of-vl-elabscopes-fix-scopes

(defthm vl-elabscopes-push-scope-fn-of-vl-elabscopes-fix-scopes
  (equal (vl-elabscopes-push-scope-fn x (vl-elabscopes-fix scopes)
                                      allow-empty)
         (vl-elabscopes-push-scope-fn x scopes allow-empty)))

Theorem: vl-elabscopes-push-scope-fn-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-elabscopes-push-scope-fn-vl-elabscopes-equiv-congruence-on-scopes
 (implies
   (vl-elabscopes-equiv scopes scopes-equiv)
   (equal (vl-elabscopes-push-scope-fn x scopes allow-empty)
          (vl-elabscopes-push-scope-fn x scopes-equiv allow-empty)))
 :rule-classes :congruence)