how to specify rewriting 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 make the rewriter dive into the
body of an eligible lambda object, both (:executable-counterpart
rewrite-lambda-modep) and (:definition rewrite-lambda-modep) must be
enabled in the then-current theory. The 0-ary function
rewrite-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
The expression (rewrite-lambda-objects-theory) macroexpands to the
(e/d ((:executable-counterpart rewrite-lambda-modep)
which is a theory equal to then current theory except that the
executable-counterpart rune and the definition rune of
rewrite-lambda-modep are enabled. This expansion is suitable for use in
an in-theory event or :in-theory hint (see :hints).
Both these two runes are initally enabled, so eligible lambda object
bodies are rewritten by default until and unless some event (e.g., an in-theory or include-book) or a superior local subgoal hint changes
the status of those runes.
For example, if lambda object rewriting has been disabled globally
and you wish to enable it for Subgoal 3 of some proof, you could use
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 allow
rewriting of lambda objects, you might write
Some users might prefer
:in-theory (e/d ((:executable-counterpart rewrite-lambda-modep)
See theories for general information about theories and how to
create and use them.