|
|
|---|
|
|
|
|---|
A macro that causes RP-Rewriter to throw a readable error when a certain pattern occurs.
In cases where users want to make sure that a term of a certain pattern does not occur, or it is taken care of by a rewrite rule with higher priority.
(def-rw-opener-error <name> ;; a unique name for the opener error rule <pattern> ;; a pattern to match/unify ;;optional keys :do-not-print (a b c ...) ;; a list of variables not to print when ;; RP-Rewriter encounters the term and ;; unifies with variables. Default: nil. :disabled <t-or-nil> ;; whether or not opener error rule should be ;; disabled. :message "..." ;; A user defined message if user wants to ;; override the original. )
A def-rw-opener-error event will submit a disabled rewrite rule with defthm, but it will be enabled in RP-Rewriter's rule-set by default. Such rules might be useful if you are using some rewrite rules with hypotheses and want to make sure that hypotheses are relieved, otherwise this rule will be used and RP-Rewriter will throw an eligible error.