Major Section: THEORIES
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.
Examples: (e/d (lemma1 lemma2)) ; equivalent to (enable lemma1 lemma2) (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)) [etc.] (in-theory (enable . enables-n)) (in-theory (disable . disables-n))
