		Search-engine friendly clone of the ACL2 documentation.

Scopetree

Scopetree->leaves

Get the leaves field from a scopetree.

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

This is an ordinary field accessor created by defprod.

Definitions and Theorems

Function: scopetree->leaves$inline

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

Theorem: name-alist-p-of-scopetree->leaves

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

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

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

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

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