|
|
|---|
|
|
|
|---|
Execute a block.
(exec-block stmts env limit) → val?+denv
The block consists of a list of statements, which are supplied to this ACL2 function. We first push a new empty scope for variables and constants; then we execute the statements, propagating any return value. If there is no return value, we pop the scope we pushed before.