		Search-engine friendly clone of the ACL2 documentation.

Valid-dirabsdeclor

Validate a direct abstract declarator.

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

This is fairly similar to valid-dirdeclor (see that function's documentation), but since the direct declarator is abstract, there is no identifier being declared to return. Furthermore, there is no flag for function definitions, since a function definition uses a (direct) declarator, not an (direct) abstract declarator.