• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • 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
        • 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

    Rule-names

    How rules are named.

    Examples:
    (:rewrite assoc-of-app)
    (:linear delta-aref . 2)
    (:definition length)
    (:executable-counterpart length)

    See rune.