		Search-engine friendly clone of the ACL2 documentation.

Check-expression-list

Check if a list of expressions is statically well-formed.

Signature
(check-expression-list exprs ctxt) → result
Arguments: exprs — Guard (expression-listp exprs).; ctxt — Guard (contextp ctxt).
Returns: result — Type (type-resultp result).

We require each expression to be single-valued. So the list of types in the type result consists of the types of the expressions, in order.

Definitions and Theorems

Theorem: len-of-result-types

(defthm len-of-result-types
  (b* ((?result (check-expression-list exprs ctxt)))
    (implies (type-result-case result :ok)
             (equal (len (type-result-ok->types result))
                    (len exprs)))))