PURE_REWRITE_CONV

Rewrite.PURE_REWRITE_CONV : (thm list -> conv)

Rewrites a term with only the given list of rewrites.

This conversion provides a method for rewriting a term with the theorems given, and excluding simplification with tautologies in implicit_rewrites. Matching subterms are found recursively, until no more matches are found. For more details on rewriting see GEN_REWRITE_CONV.

PURE_REWRITE_CONV is useful when the simplifications that arise by rewriting a theorem with implicit_rewrites are not wanted.

Failure

Does not fail. May result in divergence, in which case PURE_ONCE_REWRITE_CONV can be used.

See also

Rewrite.GEN_REWRITE_CONV, Rewrite.ONCE_REWRITE_CONV, Rewrite.PURE_ONCE_REWRITE_CONV, Rewrite.REWRITE_CONV