Major Section: EVENTS
We assume familiarity with theories; in particular, see in-theory for the normal way to set the current theory. Here, we discuss an analogous event that pertains only to non-linear arithmetic (see non-linear-arithmetic).
Example: (in-arithmetic-theory '(lemma1 lemma2)) General Form: (in-arithmetic-theory term :doc doc-string)where
termis a term that when evaluated will produce a theory (see theories), and
doc-stringis an optional documentation string not beginning with ``
:Doc-Section...''. Except for the variable
termmust contain no free variables.
Termis evaluated with the variable
worldbound to the current world to obtain a theory and the corresponding runic theory (see theories) is then used by non-linear arithmetic (see non-linear-arithmetic).
term involves macros such as
you will probably not get what you expect! Those macros are defined
relative to the
CURRENT-THEORY. But in this context you might
wish they were defined in terms of the ``
which is not actually a defined function. We do not anticipate that users
will repeatedly modify the arithmetic theory. We expect
term most often
to be a constant list of runes and so have not provided ``arithmetic theory
manipulation functions'' analogous to
Because no unique name is associated with an
there is no way we can store the documentation string
in our il[documentation] database. Hence, we actually prohibit
from having the form of an ACL2 documentation string;