|
|
|---|
|
|
|
|---|
Check if a list of expressions is safe.
(check-safe-expression-list exprs varset funtab) → number?
If successful, return the number of expressions. The caller can obtain this number directly from the list of expressions, but in the future this ACL2 function will likely return the list of types of the expressions, so we prefer to have already that kind of structure here.
We check each expression in turn. Each expression must return exactly one result.