		Search-engine friendly clone of the ACL2 documentation.

E/d

Enable/disable rules

The macro e/d creates theory expressions for use in in-theory hints and events. It provides a convenient way to enable and disable simultaneously, without having to write arcane theory expressions. For related utilities, see enable and see disable.

Examples:
(e/d (lemma1 (:e fn)))         ; equivalent to (enable lemma1 (:e fn))
(e/d () (lemma))               ; equivalent to (disable lemma)
(e/d (lemma1) (lemma2 lemma3)) ; Enable lemma1 then disable lemma2, lemma3.
(e/d () (lemma1) (lemma2))     ; Disable lemma1 then enable lemma2.

General Form:
(e/d enables-0 disables-0 ... enables-n disables-n)

where each enables-i and disables-i is a list of runic designators; see theories, see enable, and see disable. Note that the concluding disables-n may be omitted.

The e/d macro takes any number of lists suitable for the enable and disable macros. The event

(in-theory (e/d (e00 e01 e02 ...) (d00 d01 d02 ...)
                ...
                (en0 en1 en2 ...) (dn0 dn1 dn2 ...)

creates a theory that is equivalent to the following sequence of in-theory events. (An analogous similar effect takes place for :in-theory hints.

(in-theory (enable e00 e01 e02 ...))
(in-theory (disable d00 d01 d02 ...))
...
(in-theory (enable en0 en1 en2 ...))
(in-theory (disable dn0 dn1 dn2 ...))