Mathlib v3 is deprecated. Go to Mathlib v4

Inductive tactic.rewrite_search.using_conv.splice_result

Modification history

2021-01-06 11:04
src/tactic/rewrite_search/explain.lean
feat(tactic/rewrite_search): Automatically searching for chains of rewrites (#4841) …
Added tactic.rewrite_search.using_conv.splice_resultView on Github →