Major Section: EVENTS
Example: (in-theory (set-difference-theories (universal-theory :here) '(flatten (:executable-counterpart flatten)))) General Form: (in-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...''. Because no unique name is associated with an
in-theoryevent, there is no way we can store the documentation string
doc-stringin our documentation database. Hence, we actually prohibit
doc-stringfrom having the form of an ACL2 documentation string; see doc-string.
Except for the variable
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-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. See theory-functions for a list
of the commonly used theory manipulation functions.
Note that it is often useful to surround
in-theory events with
local, that is, to use
(local (in-theory ...)). This use of
encapsulate events and books will prevent the
effect of this theory change from being exported outside the context of that
encapsulate or book.
Also see hints for a discussion of the
:in-theory hint, including some
explanation of the important point that an
:in-theory hint will always be
evaluated relative to the current ACL2 logical world, not relative to
the theory of a previous goal.
In-theory returns an error triple (see error-triples). When the
return is without error, the value is of the form
(mv nil (:NUMBER-OF-ENABLED-RUNES k) state) where
k is the length of
the new current theory. This value of
k is what is printed when an
in-theory event evaluates without error at the top level.