Set-enforce-redundancy
Require most events to be redundant
General Forms:
(set-enforce-redundancy nil) ; do not require redundancy (default)
(set-enforce-redundancy t) ; most events (see below) must be redundant
(set-enforce-redundancy :warn) ; warn for most non-redundant 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.
General Form:
(set-enforce-redundancy flag)
where flag is nil, t, or :warn, as indicated above.
This macro is essentially equivalent to
(table acl2-defaults-table :enforce-redundancy flag)
and hence is local to any books and encapsulate
events in which it occurs; see ACL2-defaults-table. However,
unlike the above simple call of the table event function (see table), no output results from a set-enforce-redundancy event.
Set-enforce-redundancy may be thought of as an event that merely sets
a flag as indicated above, which determines whether most events,
including defun and defthm events, are allowed to be
redundant; see redundant-events. The exceptions are deflabel,
defpkg, encapsulate, include-book, push-untouchable, remove-untouchable, set-body, and table events. Any other type of non-redundant event will cause an
error if flag is t and a warning if flag is nil,
except in the course of carrying out an include-book form or
the second pass of an encapsulate form.
Note that because table events that set the ACL2-defaults-table are implicitly local, set-enforce-redundancy
events are ignored when including books. However, the presence of the event
(set-enforce-redundancy t) in a book guarantees that its subsequent
definitions and theorems are redundant. This can be a useful property to
maintain in library development, as we now describe.
An example of the use of this form can be found in the community books under directory books/rtl/rel4/. The intention in that directory
has been to put all the gory details in subdirectories support/ and
arithmetic/, so that the books in subdirectory lib/ contain only the
``exported'' definitions and theorems. This approach is useful for human
readability. Moreover, suppose we want to prove new theorems in lib/.
Typically we wish to prove the new theorems using the existing books in
lib/; however, our methodology demands that the proofs go into books in
support/. If every theorem in lib/ is redundant, then we can
develop the proofs in lib/ but then when we are done, move
each book with such proofs into support/ as follows. In any such book,
we first replace include-book forms referring to books in lib/ by
include-book forms referring to corresponding books in support/
and/or arithmetic/. Then, we add suitable in-theory events to
get us back into the original lib/ proof environment.
The default behavior of the system is as though the
:enforce-redundancy value is nil. The current behavior can be
ascertained by evaluating the following form.
(cdr (assoc-eq :enforce-redundancy (table-alist 'acl2-defaults-table wrld)))
