• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
        • Rune
        • In-theory
        • Disable
        • Enable
        • Theories-and-primitives
        • Deftheory
        • Deftheory-static
        • Current-theory
        • Theory-functions
        • Rulesets
        • Theory
        • Disabledp
        • Universal-theory
        • Using-enabled-rules
        • Active-runep
        • Executable-counterpart-theory
        • Function-theory
        • E/d
          • Set-difference-theories
          • Minimal-theory
          • Ground-zero
          • Union-theories
          • Intersection-theories
          • Incompatible
          • Defthy
          • Incompatible!
          • Active-or-non-runep
          • Rule-names
        • Rule-classes
        • Proof-builder
        • Hons-and-memoization
        • Events
        • History
        • Parallelism
        • Programming
        • Real
        • ACL2-tutorial
        • Debugging
        • Miscellaneous
        • Prover-output
        • Built-in-theorems
        • Macros
        • Interfacing-tools
        • About-ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Theories
    • Theory-functions

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