Check if a structure or union specifier has no members, returning the name if the check passes.
(check-strunispec-no-members strunispec) → ident?
If the specifier is empty (i.e. has no members or name), we throw a hard error, because the specifier does not conform to the concrete syntax.
Function:
(defun check-strunispec-no-members (strunispec) (declare (xargs :guard (strunispecp strunispec))) (let ((__function__ 'check-strunispec-no-members)) (declare (ignorable __function__)) (b* (((strunispec strunispec) strunispec) ((when strunispec.members) nil) ((unless strunispec.name) (raise "Misusage error: empty structure or union specifier."))) strunispec.name)))
Theorem:
(defthm ident-optionp-of-check-strunispec-no-members (b* ((ident? (check-strunispec-no-members strunispec))) (ident-optionp ident?)) :rule-classes :rewrite)
Theorem:
(defthm check-strunispec-no-members-of-strunispec-fix-strunispec (equal (check-strunispec-no-members (strunispec-fix strunispec)) (check-strunispec-no-members strunispec)))
Theorem:
(defthm check-strunispec-no-members-strunispec-equiv-congruence-on-strunispec (implies (strunispec-equiv strunispec strunispec-equiv) (equal (check-strunispec-no-members strunispec) (check-strunispec-no-members strunispec-equiv))) :rule-classes :congruence)