: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.
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 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-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.
Because no unique name is associated with an in-theory event, there
is no way we can store the documentation string doc-string in our
documentation data base. Hence, we actually prohibit doc-string
from having the form of an ACL2 documentation string;
see doc-string.
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.