		Search-engine friendly clone of the ACL2 documentation.

Valid-decl-spec-list

Validate a list of declaration specifiers.

Signature
(valid-decl-spec-list declspecs type? tyspecs storspecs table ienv) → (mv erp new-declspecs type all-storspecs return-types new-table)
Arguments: declspecs — Guard (decl-spec-listp declspecs).; type? — Guard (type-optionp type?).; tyspecs — Guard (type-spec-listp tyspecs).; storspecs — Guard (stor-spec-listp storspecs).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-declspecs — Type (decl-spec-listp new-declspecs).; type — Type (typep type).; all-storspecs — Type (stor-spec-listp all-storspecs).; 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, and the list of storage class specifiers extracted from the declaration specifiers.

We go through each element of the list, threading the partial results through. When we reach the end of the list, if a type has been determined, we return it. Otherwise, we use a separate function to attempt to determine it from the collected type specifiers.

Definitions and Theorems

Theorem: valid-decl-spec-list.all-storspecs-type-prescription

(defthm valid-decl-spec-list.all-storspecs-type-prescription
  (b* (((mv acl2::?erp ?new-declspecs ?type
            ?all-storspecs ?return-types ?new-table)
        (valid-decl-spec-list declspecs
                              type? tyspecs storspecs table ienv)))
    (true-listp all-storspecs))
  :rule-classes :type-prescription)