|
|
|---|
|
|
|
|---|
A formalization of ACL2 programs.
For now we formalize an ACL2 program as consisting of a list of packages and a set of functions. This should suffice for our initial purposes, but we will extend this notion of ACL2 program as needed.
This notion of program captures part of the ACL2 environment in which ACL2 code executes. The list of packages captures the package definitions, in the order in which they appear in the ACL2 world. The set of functions captures the function definitions, without considering their order in the ACL2 world; note that, due to mutually recursive functions, we do not quite have a total ordering on functions in the world, but rather a total ordering of mutually recursive function cliques.