		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-update-subscope

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

Definitions and Theorems

Function: vl-elabscopes-update-subscope-fn

(defun vl-elabscopes-update-subscope-fn
       (key subscope scopes allow-empty)
 (declare (xargs :guard (and (vl-elabkey-p key)
                             (vl-elabscope-p subscope)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-elabscopes-update-subscope))
  (declare (ignorable __function__))
  (b*
   ((scopes (vl-elabscopes-fix scopes))
    ((when (consp scopes))
     (cons
      (cons
          (caar scopes)
          (vl-elabscope-update-subscope key subscope (cdar scopes)))
      (cdr scopes))))
   (and (not allow-empty)
        (raise "Can't get root scope of empty elabscopes")))))

Theorem: vl-elabscopes-p-of-vl-elabscopes-update-subscope

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

Theorem: vl-elabscopes-update-subscope-fn-of-vl-elabkey-fix-key

(defthm vl-elabscopes-update-subscope-fn-of-vl-elabkey-fix-key
 (equal
      (vl-elabscopes-update-subscope-fn (vl-elabkey-fix key)
                                        subscope scopes allow-empty)
      (vl-elabscopes-update-subscope-fn
           key subscope scopes allow-empty)))

Theorem: vl-elabscopes-update-subscope-fn-vl-elabkey-equiv-congruence-on-key

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

Theorem: vl-elabscopes-update-subscope-fn-of-vl-elabscope-fix-subscope

(defthm
      vl-elabscopes-update-subscope-fn-of-vl-elabscope-fix-subscope
 (equal
   (vl-elabscopes-update-subscope-fn key (vl-elabscope-fix subscope)
                                     scopes allow-empty)
   (vl-elabscopes-update-subscope-fn
        key subscope scopes allow-empty)))

Theorem: vl-elabscopes-update-subscope-fn-vl-elabscope-equiv-congruence-on-subscope

(defthm
 vl-elabscopes-update-subscope-fn-vl-elabscope-equiv-congruence-on-subscope
 (implies (vl-elabscope-equiv subscope subscope-equiv)
          (equal (vl-elabscopes-update-subscope-fn
                      key subscope scopes allow-empty)
                 (vl-elabscopes-update-subscope-fn
                      key subscope-equiv scopes allow-empty)))
 :rule-classes :congruence)

Theorem: vl-elabscopes-update-subscope-fn-of-vl-elabscopes-fix-scopes

(defthm vl-elabscopes-update-subscope-fn-of-vl-elabscopes-fix-scopes
  (equal (vl-elabscopes-update-subscope-fn
              key subscope (vl-elabscopes-fix scopes)
              allow-empty)
         (vl-elabscopes-update-subscope-fn
              key subscope scopes allow-empty)))

Theorem: vl-elabscopes-update-subscope-fn-vl-elabscopes-equiv-congruence-on-scopes

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