|
|
|---|
|
|
|
|---|
A formalization of ACL2 packages.
Packages are defined via defpkg in ACL2. Its arguments are the name of the package, a term that evaluates to the import list of the package, and an optional documentation string.
In our formalization, we ignore the documentation string, and we consider the evaluated import list (as opposed to the term that evaluates to it). Thus, we introduce a notion of package as consisting of a package name and a list of symbol values.
Here we allow any string as package name, despite the restrictions given in defpkg. Those restrictions can be captured elsewhere.