		Search-engine friendly clone of the ACL2 documentation.

Valid-genassoc-list

Validate a list of generic associations.

Signature
(valid-genassoc-list genassocs table ienv) → (mv erp new-genassocs type-alist return-types new-table)
Arguments: genassocs — Guard (genassoc-listp genassocs).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-genassocs — Type (genassoc-listp new-genassocs).; type-alist — Type (type-option-type-alistp type-alist).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

We validate each generic association, one after the other. We put the calculated types (and optional types) into an alist, which we return. There may be repeated keys in the alist: it is a feature, so we can separately check their uniqueness.

Definitions and Theorems

Theorem: alistp-of-valid-genassoc-list.type-alist

(defthm alistp-of-valid-genassoc-list.type-alist
  (b* (((mv acl2::?erp ?new-genassocs
            ?type-alist ?return-types ?new-table)
        (valid-genassoc-list genassocs table ienv)))
    (alistp type-alist)))