		Search-engine friendly clone of the ACL2 documentation.

Valid-enumspec

Validate an enumeration specifier.

Signature
(valid-enumspec enumspec table ienv) → (mv erp new-enumspec return-types new-table)
Arguments: enumspec — Guard (enumspecp enumspec).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: new-enumspec — Type (enumspecp new-enumspec).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

We check that there is at least a name of a list of enumerators; although this is a syntactic constraint, it is currently not captured in our abstract syntax, so we double-check it here.

For now our validation tabled include no information about enumeration tags, so we do not extend the validation table, if the enumeration specifier has a name. However, we validate the enumerators, if present.