Hands-off-lambda-objects-theory
how to specify no modification of lambda objects
The enabled status of two rewrite-lambda-modep runes are used
as flags to determine the action taken when eligible lambda objects are
encountered by the ACL2 rewriter. See rewrite-lambda-object and
rewrite-lambda-object-actions. To prevent the rewriter even
considering changing a quoted lambda object, the rune
(:executable-counterpart rewrite-lambda-modep) must be disabled in the
then-current theory. The 0-ary function hands-off-lambda-objects-theory
returns such a theory.
In fact, diving into eligible quoted lambda object constants to
rewrite the body is the default action when ACL2 starts up. See rewriting-versus-cleaning-up-lambda-objects for why you might want to change
the default action when eligible lambda objects are encountered by the
rewriter.
The expression (hands-off-lambda-objects-theory) macroexpands to the
theory expression
(e/d nil
((:executable-counterpart rewrite-lambda-modep)))
which is a theory equal to then current theory except that the
executable-counterpart rune of rewrite-lambda-modep is disabled. This
expansion is suitable for use in an in-theory event or
:in-theory hint (see :hints).
This rune is initally enabled, so eligible lambda object bodies are
either rewritten or syntactically cleaned by default (depending on the status
of (:definition rewrite-lambda-modep)) until and unless some
event (e.g., an in-theory or include-book) or a superior
local subgoal hint changes the status of this rune.
For example, if lambda object rewriting is active and you wish it not
to be (so that lambda objects remain unchanged) in Subgoal 3 of
some proof, you could use the :hints
("Subgoal 3"
:in-theory (hands-off-lambda-objects-theory))
Note that if you also wish to enable or disable other runes in the same
subgoal you must construct an appropriate theory.
For example, if in Subgoal 3 of some proof you wanted to enable
LEMMA1 and disable LEMMA2 in a theory that will also specify
syntactic cleaning of lambda objects, you might write
("Subgoal 3"
:in-theory (set-difference-theories
(union-theories (hands-off-lambda-objects-theory)
'(LEMMA1))
'(LEMMA2)))
Some users might prefer
("Subgoal 3"
:in-theory (e/d (LEMMA1)
((:executable-counterpart rewrite-lambda-modep)
LEMMA2)))
See theories for general information about theories and how to
create and use them.
