• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
      • Gl
      • Witness-cp
      • Ccg
      • Install-not-normalized
      • Rewrite$
      • Fgl
      • Removable-runes
      • Efficiency
      • Rewrite-bounds
      • Bash
      • Def-dag-measure
      • Bdd
      • Remove-hyps
      • Contextual-rewriting
      • Simp
      • Rewrite$-hyps
      • Bash-term-to-dnf
      • Use-trivial-ancestors-check
      • Minimal-runes
      • Clause-processor-tools
        • Rp-rewriter
          • Rp-ruleset
          • Defthmrp
          • Rp-rewriter/meta-rules
          • Rp-utilities
            • Defthmrp
            • Show-rules
            • Def-rw-opener-error
            • Valid-sc
            • Set-rp-backchain-limit
            • Fetch-new-theory
            • Ex-from-rp
            • Rp-other-utilities
              • Rule-syntaxp
              • Add-rp-rule
              • Falist-consistent
              • Defthm-lambda
              • Def-rp-thm
            • Rp-equal
            • Preserve-current-theory
            • Set-rw-step-limit
            • Rp-termp
            • Include-fnc
            • Set-rp-backchain-limit-throws-error
            • Defwarrant-rp
            • Create-case-match-macro
          • Rp-rewriter-demo
          • Rp-rewriter/debugging
          • Rp-rewriter/applications
      • Fn-is-body
      • Without-subsumption
      • Rewrite-equiv-hint
      • Def-bounds
      • Rewrite$-context
      • Try-gl-concls
      • Hint-utils
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Rp-utilities

Rp-other-utilities

Some names that are aliases to other tools

Subtopics

Rule-syntaxp
Syntax check for a 'rule' defined with rp::custom-rewrite-rule. If warning key is set to non-nil, a warning is issued for failures.
Add-rp-rule
Register a rule with RP-Rewriter
Falist-consistent
Given a falist term (falist * *), checks consistence of arguments.
Defthm-lambda
defthm-lambda is deprecated. Please see defthmrp, add-rp-rule, or lambda-opt for relevant topics.
Def-rp-thm
Same as defthmrp