		Search-engine friendly clone of the ACL2 documentation.

Valid-tyname

Validate a type name.

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

A valid type name denotes a type, so we return a type if validation is successful.

First we validate the list of specifiers and qualifiers, which returns a type if successful. Then we validate the optional abstract declarator, which returns a possibly refined type. We return the latter type.