		Search-engine friendly clone of the ACL2 documentation.

Dimb-enumspec

Disambiguate an enumeration specifier.

Signature
(dimb-enumspec enumspec table) → (mv erp new-enumspec new-table)
Arguments: enumspec — Guard (enumspecp enumspec).; table — Guard (dimb-tablep table).
Returns: new-enumspec — Type (enumspecp new-enumspec).; new-table — Type (dimb-tablep new-table).

This also extends the disambiguation table with the names of the enumerators (i.e. enumeration constants). The scope of an enumeration constant starts just after the appearance of its enumerator [C:6.2.1/7]. The extension of the table is actually done by the function that disambiguates the enumerators.