In this file, we set up
obviously as a "replacer" tactic,
whose implementation can be modified after the fact.
Then we set the default implementation to be
Implementation note #
At present we don't actually take advantage of the replacer mechanism in mathlib.
In the past it had been used by an external category theory library which wanted to incorporate
rewrite_search as part of