		Search-engine friendly clone of the ACL2 documentation.

Valid-strunispec

Validate a structure or union specifier.

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

We check that there is at least a name or a list of members [C:6.7.2.1/2].

For now our validation tables include no information about structure and union tags, so we do not extend the validation table, if the structure or union specifier has a name. However, we validate the members, if present.