		Search-engine friendly clone of the ACL2 documentation.

Valid-param-declor

Validate a parameter declarator.

Signature
(valid-param-declor paramdeclor type table ienv) → (mv erp new-paramdeclor new-type ident? return-types uid? new-table)
Arguments: paramdeclor — Guard (param-declorp paramdeclor).; type — Guard (typep type).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-paramdeclor — Type (param-declorp new-paramdeclor).; new-type — Type (typep new-type).; ident? — Type (ident-optionp ident?).; return-types — Type (type-setp return-types).; uid? — Type (uid-optionp uid?).; 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, the identifier, and the uid. If the parameter declarator is an abstract declarator, we return the possibly refined type but no identifier nor uid. If the parameter declarator is absent, we return the type unchanged and no identifier nor uid.

Definitions and Theorems

Theorem: valid-param-declor.uid?-under-iff

(defthm valid-param-declor.uid?-under-iff
  (b* (((mv acl2::?erp ?new-paramdeclor ?new-type
            ?ident? ?return-types ?uid? ?new-table)
        (valid-param-declor paramdeclor type table ienv)))
    (implies (not erp) (iff uid? ident?))))