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