Recommendations related to enabling and disabling functions and
The best practices depend somewhat on the kind of book you are
writing. We distinguish between Widget Libraries and Core
Scenario: your library describes a particular kind of "Widget:" it defines
what Widgets are, provides some useful algorithms for operating on Widgets, and
proves some theorems about the properties of Widgets and these algorithms.
- Avoid any non-local inclusion of arithmetic libraries
- Avoid any non-local (in-theory ...) events that involve built-in ACL2
functions. For instance, do not do: (in-theory (enable append)).
- Try to respect the ACL2 namespace, e.g., do not define new functions in the
ACL2 package, especially with short or generic names, etc.
- You would expect that loading a Widget library should generally just give
you definitions and lemmas that are about Widgets.
- You would not expect a Widget library to change how you reason about other
concepts that are unrelated to Widgets.
- Non-local arithmetic includes may make your Widget library incompatible
with other arithmetic libraries.
Scenario: your library is meant to assist with reasoning about built-in ACL2
functions, for instance:
- arithmetic functions like +, -, *, /, floor, mod, logand;
- list functions like append, len, nth, member, subsetp;
- string functions like coerce, concatenate, subseq;
- system functions like io routines and state updates;
- meta functions like pseudo-termp, disjoin, conjoin-clauses;
Since your library is inherently about existing ACL2 functions rather than
new definitions, the Widget-library recommendations do not necessarily