Get the scope field from a address.
(address->scope x) → scope
This is an ordinary field accessor created by defprod.
Function:
(defun address->scope$inline (x) (declare (xargs :guard (address-p x))) (declare (xargs :guard t)) (let ((__function__ 'address->scope)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and t x))) (addr-scope-fix (if (or (atom x) (not (eq (car x) :address))) 0 (nth 3 x)))) :exec (if (or (atom x) (not (eq (car x) :address))) 0 (nth 3 x)))))
Theorem:
(defthm addr-scope-p-of-address->scope (b* ((scope (address->scope$inline x))) (addr-scope-p scope)) :rule-classes :rewrite)
Theorem:
(defthm address->scope$inline-of-address-fix-x (equal (address->scope$inline (address-fix x)) (address->scope$inline x)))
Theorem:
(defthm address->scope$inline-address-equiv-congruence-on-x (implies (address-equiv x x-equiv) (equal (address->scope$inline x) (address->scope$inline x-equiv))) :rule-classes :congruence)