		Search-engine friendly clone of the ACL2 documentation.

Scopetree

Scopetree->subscopes

Get the subscopes field from a scopetree.

Signature
(scopetree->subscopes x) → subscopes
Arguments: x — Guard (scopetree-p x).
Returns: subscopes — Type (scopetree-alist-p subscopes).

This is an ordinary field accessor created by defprod.

Definitions and Theorems

Function: scopetree->subscopes$inline

(defun scopetree->subscopes$inline (x)
  (declare (xargs :guard (scopetree-p x)))
  (declare (xargs :guard t))
  (let ((__function__ 'scopetree->subscopes))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x)))
           (scopetree-alist-fix (std::prod-cdr x)))
         :exec (std::prod-cdr x))))

Theorem: scopetree-alist-p-of-scopetree->subscopes

(defthm scopetree-alist-p-of-scopetree->subscopes
  (b* ((subscopes (scopetree->subscopes$inline x)))
    (scopetree-alist-p subscopes))
  :rule-classes :rewrite)

Theorem: scopetree->subscopes$inline-of-scopetree-fix-x

(defthm scopetree->subscopes$inline-of-scopetree-fix-x
  (equal (scopetree->subscopes$inline (scopetree-fix x))
         (scopetree->subscopes$inline x)))

Theorem: scopetree->subscopes$inline-scopetree-equiv-congruence-on-x

(defthm scopetree->subscopes$inline-scopetree-equiv-congruence-on-x
  (implies (scopetree-equiv x x-equiv)
           (equal (scopetree->subscopes$inline x)
                  (scopetree->subscopes$inline x-equiv)))
  :rule-classes :congruence)