		Search-engine friendly clone of the ACL2 documentation.

Valid-spec/qual-list

Validate a list of specifiers and qualifiers.

Signature
(valid-spec/qual-list specquals type? tyspecs table ienv) → (mv erp new-specquals type return-types new-table)
Arguments: specquals — Guard (spec/qual-listp specquals).; type? — Guard (type-optionp type?).; tyspecs — Guard (type-spec-listp tyspecs).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-specquals — Type (spec/qual-listp new-specquals).; type — Type (typep type).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

If validation is successful, we return the type determined by the type specifiers in the sequence.

We validate specifiers and qualifiers from left to right, threading the partial results through. When we reach the end, if the type has not been determined yet, we look at the collected type specifiers and determine the type, via a separate validation function. If there are no type specifiers, but no type has been determined, it means that there were no type specifiers at all [C17:6.7.2/2].