• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
      • Defun
      • Verify-guards
      • Table
      • Mutual-recursion
      • Memoize
      • Make-event
      • Include-book
      • Encapsulate
      • Defun-sk
      • Defttag
      • Defstobj
      • Defpkg
      • Defattach
      • Defabsstobj
      • Defchoose
      • Progn
      • Verify-termination
      • Redundant-events
      • Defmacro
      • Defconst
      • Skip-proofs
      • In-theory
      • Embedded-event-form
      • Value-triple
      • Comp
      • Local
      • Defthm
      • Progn!
      • Defevaluator
      • Theory-invariant
      • Assert-event
      • Defun-inline
      • Project-dir-alist
      • Partial-encapsulate
      • Define-trusted-clause-processor
      • Defproxy
      • Defexec
      • Defun-nx
      • Defthmg
      • Defpun
      • Defabbrev
      • Set-table-guard
      • Name
      • Defrec
      • Add-custom-keyword-hint
      • Regenerate-tau-database
      • Defcong
      • Deftheory
        • Rulesets
        • Defthy
      • Defaxiom
      • Deftheory-static
      • Defund
      • Evisc-table
      • Verify-guards+
      • Logical-name
      • Profile
      • Defequiv
      • Defmacro-untouchable
      • Add-global-stobj
      • Defthmr
      • Defstub
      • Defrefinement
      • Deflabel
      • In-arithmetic-theory
      • Unmemoize
      • Defabsstobj-missing-events
      • Defthmd
      • Fake-event
      • Set-body
      • Defun-notinline
      • Functions-after
      • Macros-after
      • Dump-events
      • Defund-nx
      • Defun$
      • Remove-global-stobj
      • Remove-custom-keyword-hint
      • Dft
      • Defthy
      • Defund-notinline
      • Defnd
      • Defn
      • Defund-inline
      • Defmacro-last
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Events
• Theories
• Deftheory

Defthy

Define a theory (to enable or disable a set of rules)

See deftheory. The defthy macro is simply a convenient macro for deftheory that supports a limited notion of redundancy; see redundant-events. Specifically: a call (defthy name expr) expands to the corresponding event (deftheory name expr :redundant-okp t).