		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-push-named

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

Definitions and Theorems

Function: vl-elabscopes-push-named-fn

(defun vl-elabscopes-push-named-fn (key scopes allow-empty)
 (declare (xargs :guard (and (vl-elabkey-p key)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-elabscopes-push-named))
  (declare (ignorable __function__))
  (b* ((scopes (vl-elabscopes-fix scopes))
       ((when (atom scopes))
        (and (not allow-empty)
             (raise "No outer scope -- can't push named scope!"))
        (cons (cons (vl-elabkey-fix key)
                    (make-vl-elabscope))
              scopes))
       (curr-elabscope (cdar scopes))
       (new-elabscope (or (vl-elabscope-subscope key curr-elabscope)
                          (make-vl-elabscope))))
    (cons (cons (vl-elabkey-fix key)
                new-elabscope)
          scopes))))

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

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

Theorem: vl-elabscopes-push-named-fn-of-vl-elabkey-fix-key

(defthm vl-elabscopes-push-named-fn-of-vl-elabkey-fix-key
  (equal (vl-elabscopes-push-named-fn (vl-elabkey-fix key)
                                      scopes allow-empty)
         (vl-elabscopes-push-named-fn key scopes allow-empty)))

Theorem: vl-elabscopes-push-named-fn-vl-elabkey-equiv-congruence-on-key

(defthm
     vl-elabscopes-push-named-fn-vl-elabkey-equiv-congruence-on-key
 (implies
   (vl-elabkey-equiv key key-equiv)
   (equal
        (vl-elabscopes-push-named-fn key scopes allow-empty)
        (vl-elabscopes-push-named-fn key-equiv scopes allow-empty)))
 :rule-classes :congruence)

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

(defthm vl-elabscopes-push-named-fn-of-vl-elabscopes-fix-scopes
  (equal (vl-elabscopes-push-named-fn key (vl-elabscopes-fix scopes)
                                      allow-empty)
         (vl-elabscopes-push-named-fn key scopes allow-empty)))

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

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