		Search-engine friendly clone of the ACL2 documentation.

Exec-initer

Execute an initializer.

Signature
(exec-initer initer compst fenv limit) → (mv result new-compst)
Arguments: initer — Guard (initerp initer).; compst — Guard (compustatep compst).; fenv — Guard (fun-envp fenv).; limit — Guard (natp limit).
Returns: result — Type (init-value-resultp result).; new-compst — Type (compustatep new-compst).

If the initializer consists of a single expression, the expression must be a function call or a pure expression. If it is a function call, it must return a value (not nil).

If the initializer consists of a list of expressions, the expressions must be pure, to avoid ambiguities with the order of evaluation.