def
conv.interactive.erw
:
interactive.parse tactic.interactive.rw_rules → (tactic.rewrite_cfg := {to_apply_cfg := {md := tactic.transparency.semireducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}, symm := bool.ff, occs := occurrences.all}) → conv unit
guard_target t fails if the target of the conv goal is not t.
We use this tactic for writing tests.