• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
        • Bv
        • Ihs
          • Logops-definitions
          • Math-lemmas
          • Ihs-theories
          • Ihs-init
            • Ihs-utilities
              • Defun-type/exec-theory
              • Defun-theory
              • Rewrite-free-theory
              • Definition-free-theory
              • Rewrite-theory
              • Definition-theory
              • Mlambda
              • Enable-theory
              • Disable-theory
          • Logops
        • Rtl
      • Algebra
  • Ihs-init

Ihs-utilities

Utility macros and functions used throughout the IHS books.

Subtopics

Defun-type/exec-theory
Collects and returns a special set of runes.
Defun-theory
Collects and returns a special set of runes.
Rewrite-free-theory
Returns the theory with all :REWRITE rules deleted.
Definition-free-theory
Returns the theory with all :DEFINITION rules deleted.
Rewrite-theory
Collects all of the :REWRITE runes from theory.
Definition-theory
Collects all of the :DEFINITION runes from theory.
Mlambda
Macro LAMBDA form.
Enable-theory
Creates an in-theory event that is equivalent to ENABLEing the theory-expression. Note that theory-expression is evaluated.
Disable-theory
Creates an IN-THEORY event that is equivalent to DISABLEing the theory-expression. Note that theory-expression is evaluated.