IN-ARITHMETIC-THEORY

designate ``current'' theory for some rewriting done in linear arithmetic
Major Section:  EVENTS

Example:
(in-arithmetic-theory '(lemma1 lemma2))

General Form: (in-arithmetic-theory term :doc doc-string)

where term is a term that when evaluated will produce a theory (see theories), and doc-string is an optional documentation string not beginning with ``:doc-section ...''. 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 made the current theory. Thus, immediately after the in-arithmetic-theory, a rule is enabled iff its rule name is a member of the runic interpretation (see theories) of some member of the value of term.

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.

BECAUSE NO UNIQUE name is associated with an in-arithmetic-theory event, there is no way we can store the documentation string doc-string in our il[documentation] data base. Hence, we actually prohibit doc-string from having the form of an ACL2 documentation string; see doc-string.

See non-linear-arithmetic.