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.
The e/d macro takes any number of lists suitable for the enable and disable macros, and creates a theory that is equal to
(current-theory :here) after executing the following commands.
(in-theory (enable . enables-0))
(in-theory (disable . disables-0))
...
(in-theory (enable . enables-n))
(in-theory (disable . disables-n))
