		Search-engine friendly clone of the ACL2 documentation.

Exec

Exec-block

Execute a block.

Signature
(exec-block block cstate funenv limit) → outcome
Arguments: block — Guard (blockp block).; cstate — Guard (cstatep cstate).; funenv — Guard (funenvp funenv).; limit — Guard (natp limit).
Returns: outcome — Type (soutcome-resultp outcome).

We save (the names of) the variables just before the block, so that we can restrict the computation state after the block to only those variables, as explained in restrict-vars. We extend the function environment with the functions in the block. We execute the block's statements. We return the resulting outcome, but we remove all the variables added by the block.