SET-ENFORCE-REDUNDANCY

require most events to be redundant 
Major Section:  SWITCHES-PARAMETERS-AND-MODES


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.

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)))