world. When theory expressions
are evaluated by in-theory or the :in-theory hint, world is bound to
the current ACL2 world.
Major Section: THEORIES
Examples: (current-theory :here) (current-theory 'lemma3)See logical-name.
General Form: (current-theory logical-name)Returns the current theory as it existed immediately after the introduction of
logical-name provided it is evaluated in
an environment in which the variable symbol WORLD is bound to the
current ACL2 logical world, (w state). Thus,
ACL2 !>(current-theory :here)will cause an (unbound variable) error while
ACL2 !>(let ((world (w state))) (current-theory :here))will return the current theory in world.
See theories and see logical-name for a discussion of
theories in general and why the commonly used ``theory functions''
such as current-theory are really macros that expand into terms
involving the variable world.
The theory returned by current-theory is in fact the theory selected by
the in-theory event most recently preceding logical name, extended by
the rules introduced up through logical-name.
You may experience a fencepost problem in deciding which logical
name to use. Deflabel can always be used to mark unambiguously for
future reference a particular point in the development of your
theory. The order of events in the vicinity of an encapsulate is
confusing. See encapsulate.
This ``function'' is actually a macro that expands to a term
mentioning the single free variable world. When theory expressions
are evaluated by in-theory or the :in-theory hint, world is bound to
the current ACL2 world.