		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Check-enum-spec-no-list

Check if an enumeration union specifier has no enumerators, returning the name if the check passes.

Signature
(check-enum-spec-no-list enumspec) → ident?
Arguments: enumspec — Guard (enum-specp enumspec).
Returns: ident? — Type (ident-optionp 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.

Definitions and Theorems

Function: check-enum-spec-no-list

(defun check-enum-spec-no-list (enumspec)
  (declare (xargs :guard (enum-specp enumspec)))
  (let ((__function__ 'check-enum-spec-no-list))
    (declare (ignorable __function__))
    (b* (((enum-spec enumspec) enumspec)
         ((when enumspec.enumers) nil)
         ((unless enumspec.name?)
          (raise "Misusage error: empty enumeration specifier.")))
      enumspec.name?)))

Theorem: ident-optionp-of-check-enum-spec-no-list

(defthm ident-optionp-of-check-enum-spec-no-list
  (b* ((ident? (check-enum-spec-no-list enumspec)))
    (ident-optionp ident?))
  :rule-classes :rewrite)

Theorem: check-enum-spec-no-list-of-enum-spec-fix-enumspec

(defthm check-enum-spec-no-list-of-enum-spec-fix-enumspec
  (equal (check-enum-spec-no-list (enum-spec-fix enumspec))
         (check-enum-spec-no-list enumspec)))

Theorem: check-enum-spec-no-list-enum-spec-equiv-congruence-on-enumspec

(defthm
     check-enum-spec-no-list-enum-spec-equiv-congruence-on-enumspec
  (implies (enum-spec-equiv enumspec enumspec-equiv)
           (equal (check-enum-spec-no-list enumspec)
                  (check-enum-spec-no-list enumspec-equiv)))
  :rule-classes :congruence)