|
|
|---|
|
|
|
|---|
Convention for packages of generated symbols
ACL2 utilities, whether defined in the ACL2 sources or in books,
will ideally provide the following default behavior when feasible: generated
symbols should be in the current-package. This is the ACL2 version of
the general principle enforced by almost all programming languages: names
introduced are, by default, in the current namespace. We do not claim that
ACL2 currently adheres to this principle in all cases, but our hope that this
situation is improved over time. Indeed, the utilities defequiv,
defrefinement and defcong have been improved to conform to
this principle; see note-8-3. We hope that future utilities, not only
in ACL2 but also in the community-books, will respect this principle
when feasible. Conforming to this principle requires using make-event
in a top level form to determine the current-package from state and then passing this package to functions that generate symbols. The
section