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