|
|
|---|
|
|
|
|---|
A program-mode interpreter.
We introduce an executable program-mode function that exhaustively calls step; this program-mode function may not terminate. Then we define a wrapper that initializes the evaluation state with a function symbol and a list of argument values, same as the non-executable exec-call function. This can be used as an interpreter for the ACL2 programming language as formalized here.