		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-push-anon

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

Definitions and Theorems

Function: vl-elabscopes-push-anon-fn

(defun vl-elabscopes-push-anon-fn (scope scopes allow-empty)
  (declare (xargs :guard (and (vl-elabscope-p scope)
                              (vl-elabscopes-p scopes))))
  (declare (ignore allow-empty))
  (let ((__function__ 'vl-elabscopes-push-anon))
    (declare (ignorable __function__))
    (cons (cons nil (vl-elabscope-fix scope))
          (vl-elabscopes-fix scopes))))

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

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

Theorem: vl-elabscopes-push-anon-fn-of-vl-elabscope-fix-scope

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

Theorem: vl-elabscopes-push-anon-fn-vl-elabscope-equiv-congruence-on-scope

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

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

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

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

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