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. )