Get the env field from a funinfo+funenv.
(funinfo+funenv->env x) → env
This is an ordinary field accessor created by fty::defprod.
Function:
(defun funinfo+funenv->env$inline (x) (declare (xargs :guard (funinfo+funenv-p x))) (declare (xargs :guard t)) (let ((__function__ 'funinfo+funenv->env)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and t x))) (funenv-fix (cdr (std::da-nth 1 x)))) :exec (cdr (std::da-nth 1 x)))))
Theorem:
(defthm funenvp-of-funinfo+funenv->env (b* ((env (funinfo+funenv->env$inline x))) (funenvp env)) :rule-classes :rewrite)
Theorem:
(defthm funinfo+funenv->env$inline-of-funinfo+funenv-fix-x (equal (funinfo+funenv->env$inline (funinfo+funenv-fix x)) (funinfo+funenv->env$inline x)))
Theorem:
(defthm funinfo+funenv->env$inline-funinfo+funenv-equiv-congruence-on-x (implies (funinfo+funenv-equiv x x-equiv) (equal (funinfo+funenv->env$inline x) (funinfo+funenv->env$inline x-equiv))) :rule-classes :congruence)