In-arithmetic-theory
Designate theory for some rewriting done for non-linear arithmetic
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)
where term is a term that when evaluated will produce a theory (see
theories). Except for the variable world, term must
contain no free variables. Term is evaluated with the variable world bound 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).
Warning: If term involves macros such as enable and disable 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 ``CURRENT-ARITHMETIC-THEORY'' 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 current-theory and enable.
See non-linear-arithmetic.
