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