Major Section: EVENTS
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
the special-purpose nth/update-nth rewriter (nu-rewriter).
The flag may have one of three values: nil, t, or :literals.
: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
The value 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
with an 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
with an nth.
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
set to :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.
We expect to write more documentation as we gain experience with the
nu-rewriter.