		Search-engine friendly clone of the ACL2 documentation.

Defthmrp

A defthm macro that calls RP-Rewriter as a clause processor with some capabilities.

RP::Defthmrp is a macro that calls defthm with RP-Rewriter as a clause-processor. It may also take some of the following parameters:


 (rp::defthmrp
  <new-rule-name>
  <conjecture>
  ;; optional keys:
  :rule-classes <...>   ;; default: :rewrite
  :new-synps <...>      ;; for advanced users; can attach syntaxp to some existing
                        ;; rewrite rules. Default: nil
  :enable-meta-rules (meta-fnc1 meta-fnc2 ...) ;; an unquoted list of names
                                               ;; of meta functions that users
                                               ;; wants to enable.
  :disable-meta-rules (meta-fnc1 meta-fnc2 ...) ;; same as above
  :enable-rules (append '(rule1 rule2)
                        *rules3*
                        ...) ;; List of rule-names that users wants enabled in
      ;; RP-Rewriter's rule-set. The macro will execute the expressions first to
      ;; generate the names.
  :disable-rules <...>      ;; Same as above
  :runes '(rule1 rule2 ...) ;; When nil, the macro uses the existing rule-set of
      ;; RP-rewriter. Otherwise, it will overrride everything else regarding rules
      ;; and use only the rules given in this list.
  )