• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
          • Expand-ruleset
          • E/d*
          • Ruleset
            • Def-ruleset
            • Get-ruleset
            • Disable*
            • Def-ruleset!
            • Enable*
            • Add-to-ruleset
          • 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
        • Recursion-and-induction
        • Hons-and-memoization
        • Events
        • Parallelism
        • History
        • Programming
        • Operational-semantics
        • Real
        • Start-here
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Rulesets

    Ruleset

    The ruleset associated with a given name

    See rulesets for an introduction to rulesets.

    Examples of calls of ruleset:

    (ruleset 'my-ruleset) ; assumes that WORLD is bound
    (ruleset 'my-ruleset (w state)) ; ruleset currently associated with MY-RULESET

    Also see get-ruleset. For a more powerful operator that recursively expands ruleset names within a given ruleset, see expand-ruleset.