Advanced rewriting tactics #
This file provides three interactive tactics that give the user more control over where to perform a rewrite.
Main definitions #
nth_rewrite n rules: performs only the
nth possible rewrite using the
nth_rewrite_lhs: as above, but only rewrites on the left hand side of an equation or iff.
nth_rewrite_rhs: as above, but only rewrites on the right hand side of an equation or iff.
Implementation details #
There are two alternative backends, provided by
The kabstract backend is not currently available through mathlib.
The kabstract backend is faster, but if there are multiple identical occurrences of the
same rewritable subexpression, all are rewritten simultaneously,
and this isn't always what we want.
rewrite_search is much less capable on the