|
|
|---|
|
|
|
|---|
Number of steps RP-Rewriter can take when rewriting the hypothesis of a lemma
We have a different step limit than set-rw-step-limit when rewriting hypotheses of lemmas that may be applied to the current conjecture. This step limit can be changed with
. It is recomendeded to select a value far smaller than rw-step-limit (see set-rw-step-limit) or chose a very large rw-step-limit, otherwise rw-step-limit might override it during rewriting.(set-backchain-limit <number>)