		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-root

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

Definitions and Theorems

Function: vl-elabscopes-root-fn

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

Theorem: vl-elabscopes-p-of-vl-elabscopes-root

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

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

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

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

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