Major Section: SWITCHES-PARAMETERS-AND-MODES
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
This event sets a flag that controls whether the ACL2 rewriter uses
update-nth rewriter (nu-rewriter).
The flag may have one of three values:
:set-nu-rewriter-mode nil ; do not use nu-rewriter :set-nu-rewriter-mode t ; use nu-rewriter in rewriting :set-nu-rewriter-mode :literals ; use nu-rewriter in rewriting after ; a pre-pass through every literal (set-nu-rewriter-mode :literals) ; same as above
nil prevents the use of the nu-rewriter. The other two
values allow the use of the nu-rewriter.
When the flag is non-
nil and the rewriter encounters a term that
``begins with an
nth'', the nu-rewriter is applied. By ``begins
nth'' here we mean either the term is an application of
nth or is an application of some nonrecursive function or
lambda expression whose body contains an expression that begins
Note that the use of the nu-rewriter here described above is driven
by the rewriter, i.e., the nu-rewriter is applied only to terms
visited by the rewriter in its inside-out sweep. When the flag is
:literals the system makes a pre-pass through every goal
clause and applies the nu-rewriter to every subterm. The rewriter
is then used on the output of that pre-pass.
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so
recorded. Moreover, its effect is to set the
hence its effect is
local to the book or
containing it; see acl2-defaults-table.
We expect to write more documentation as we gain experience with the nu-rewriter.