		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-subscope

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

Definitions and Theorems

Function: vl-elabscopes-subscope-fn

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

Theorem: return-type-of-vl-elabscopes-subscope

(defthm return-type-of-vl-elabscopes-subscope
 (b* ((subscope (vl-elabscopes-subscope-fn key scopes allow-empty)))
   (iff (vl-elabscope-p subscope)
        subscope))
 :rule-classes :rewrite)

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

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

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

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

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

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

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

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