Get the decl field from a indname-result.
(indname-result->decl x) → decl
This is an ordinary field accessor created by defprod.
Function:
(defun indname-result->decl$inline (x) (declare (xargs :guard (indname-result-p x))) (declare (xargs :guard t)) (let ((__function__ 'indname-result->decl)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and t x))) (wire-fix (cdr x))) :exec (cdr x))))
Theorem:
(defthm wire-p-of-indname-result->decl (b* ((decl (indname-result->decl$inline x))) (wire-p decl)) :rule-classes :rewrite)
Theorem:
(defthm indname-result->decl$inline-of-indname-result-fix-x (equal (indname-result->decl$inline (indname-result-fix x)) (indname-result->decl$inline x)))
Theorem:
(defthm indname-result->decl$inline-indname-result-equiv-congruence-on-x (implies (indname-result-equiv x x-equiv) (equal (indname-result->decl$inline x) (indname-result->decl$inline x-equiv))) :rule-classes :congruence)