		Search-engine friendly clone of the ACL2 documentation.

Valid-expr-list

Validate a list of expressions.

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

We validate all the expressions, one after the other, and we return the resulting types, in the same order. We also return the union of all the return types. We also return a possibly updated validation table.

Definitions and Theorems

Theorem: len-of-valid-expr-list.types

(defthm len-of-valid-expr-list.types
  (b* (((mv acl2::?erp ?new-exprs
            ?types ?return-types ?new-table)
        (valid-expr-list exprs table ienv)))
    (implies (not erp)
             (equal (len types) (len exprs)))))