apply name

Stream: metaprogramming / tactics

[Johan Commelin]

Next noob question.
How do I fill in in

meta def foo (e : pexpr) (n : name) : tactic unit :=
_
-- should be something like `apply n %%e`

[Jannis Limperg]

You should be able to use resolve_name n to get a pexpr pn, then tactic.interactive.apply (pn e).

[Johan Commelin]

Thanks! With some help from Anne I managed to make it work