• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
        • Rune
        • In-theory
        • Disable
        • Enable
        • Theories-and-primitives
        • Deftheory
        • Theory-functions
        • Deftheory-static
        • Current-theory
        • Syntactically-clean-lambda-objects-theory
        • Hands-off-lambda-objects-theory
        • Rewrite-lambda-objects-theory
        • Rulesets
        • Theory
        • Disabledp
        • Universal-theory
        • Using-enabled-rules
        • E/d
        • Active-runep
          • Executable-counterpart-theory
          • Function-theory
          • 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
        • Start-here
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Theories

    Active-runep

    Check that a rune exists and is enabled

    Example:
    (active-runep '(:rewrite left-to-right))
    
    General Form:
    (active-runep rune &optional strict)

    where rune has the shape of a rune. This macro expands to an expression using the variables ens and state, and returns non-nil when the given rune exists and is enabled (according to the given ``enabled structure,'' ens, and the current logical world of the given state). See theory-invariant for how this macro can be of use.

    When the optional argument is nil or is omitted, then although the argument is required to have the shape of a rune, it need not be a rune. For example, if there is no rewrite rule named left-to-right, then (active-runep '(:rewrite left-to-right)) will simply return nil. If instead you'd like this call to cause an error, use a non-nil optional argument or, equivalently, use active-or-non-runep.