		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-traverse

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

Definitions and Theorems

Function: vl-elabscopes-traverse-fn

(defun vl-elabscopes-traverse-fn (trav scopes allow-empty)
  (declare (xargs :guard (and (vl-elabtraversal-p trav)
                              (vl-elabscopes-p scopes))))
  (let ((__function__ 'vl-elabscopes-traverse))
    (declare (ignorable __function__))
    (if (atom trav)
        (vl-elabscopes-fix scopes)
      (vl-elabscopes-traverse
           (cdr trav)
           (vl-elabscopes-do-instruction (car trav)
                                         scopes
                                         :allow-empty allow-empty)
           :allow-empty allow-empty))))

Theorem: vl-elabscopes-p-of-vl-elabscopes-traverse

(defthm vl-elabscopes-p-of-vl-elabscopes-traverse
 (b*
  ((new-scopes (vl-elabscopes-traverse-fn trav scopes allow-empty)))
  (vl-elabscopes-p new-scopes))
 :rule-classes :rewrite)

Theorem: vl-elabscopes-traverse-fn-of-vl-elabtraversal-fix-trav

(defthm vl-elabscopes-traverse-fn-of-vl-elabtraversal-fix-trav
  (equal (vl-elabscopes-traverse-fn (vl-elabtraversal-fix trav)
                                    scopes allow-empty)
         (vl-elabscopes-traverse-fn trav scopes allow-empty)))

Theorem: vl-elabscopes-traverse-fn-vl-elabtraversal-equiv-congruence-on-trav

(defthm
 vl-elabscopes-traverse-fn-vl-elabtraversal-equiv-congruence-on-trav
 (implies
  (vl-elabtraversal-equiv trav trav-equiv)
  (equal (vl-elabscopes-traverse-fn trav scopes allow-empty)
         (vl-elabscopes-traverse-fn trav-equiv scopes allow-empty)))
 :rule-classes :congruence)

Theorem: vl-elabscopes-traverse-fn-of-vl-elabscopes-fix-scopes

(defthm vl-elabscopes-traverse-fn-of-vl-elabscopes-fix-scopes
  (equal (vl-elabscopes-traverse-fn trav (vl-elabscopes-fix scopes)
                                    allow-empty)
         (vl-elabscopes-traverse-fn trav scopes allow-empty)))

Theorem: vl-elabscopes-traverse-fn-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-elabscopes-traverse-fn-vl-elabscopes-equiv-congruence-on-scopes
 (implies
  (vl-elabscopes-equiv scopes scopes-equiv)
  (equal (vl-elabscopes-traverse-fn trav scopes allow-empty)
         (vl-elabscopes-traverse-fn trav scopes-equiv allow-empty)))
 :rule-classes :congruence)