		Search-engine friendly clone of the ACL2 documentation.

Valid-paramdeclor

Validate a parameter declarator.

Signature
(valid-paramdeclor paramdeclor type table ienv) → (mv erp new-paramdeclor new-type ident? return-types new-table)
Arguments: paramdeclor — Guard (paramdeclorp paramdeclor).; type — Guard (typep type).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: new-paramdeclor — Type (paramdeclorp new-paramdeclor).; new-type — Type (typep new-type).; ident? — Type (ident-optionp ident?).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

The input type is the one resulting from the declaration specifiers of the parameter declaration of which the parameter declarator is part of. If validation is successful, we return a possibly refined type, and an optional identifier.

If the parameter declarator is a (non-abstract) declarator, we return the possibly refined type and the identifier. If the parameter declarator is an abstract declarator, we return the possibly refined type but no identifier. If the parameter declarator is absent, we return the type unchanged and no identifer.