		Search-engine friendly clone of the ACL2 documentation.

Redundant-events

Set-in-theory-redundant-okp

Allow in-theory events to be redundant

See redundant-events for discussion of the notion of redundant events.

General Forms:
(set-in-theory-redundant-okp nil) ; default
(set-in-theory-redundant-okp t)   ; allow in-theory events to be redundant

By default, in-theory events are never redundant. This behavior avoids a redundancy check that could be a bit expensive, as it would require computing the current theory and checking its equality to the new theory. Evaluation of the event (set-in-theory-redundant-okp t) enables that redundancy check, so that when an in-theory event computes a theory that is equal to the current theory, then that event is redundant.

To see the current setting (i.e., the default of nil or else t after evaluation of (set-in-theory-redundant-okp t)), evaluate (get-in-theory-redundant-okp state).

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 ACL2-defaults-table, and hence its effect is local to the book or encapsulate form containing it; see ACL2-defaults-table.