meta tactic with unfold

Stream: new members

[Sarah Mameche]

Is there an equivalent to 'tactic.apply' with unfold? I have a metatactic that rewrites with specific lemmas which are given as a pexpr :

meta def rw_pexpr (e : pexpr) : tactic unit :=
do e ← tactic.to_expr e,
  t ← target,
  (p,h,_) ← tactic.rewrite e t,
  replace_target p h

It works for rewriting if the pexpris a lemma, but not if it is a definition (even though doing rw with the definition interactively works). What can I do if I want to unfold the definition using the meta tactic?

[Mario Carneiro]

use get_equation_lemmas to get a list of simp lemmas for a definition