Stream: metaprogramming / tactics
Topic: apply name
Johan Commelin (Oct 28 2020 at 12:11):
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 (Oct 28 2020 at 12:54):
You should be able to use
resolve_name n to get a
tactic.interactive.apply (pn e).
Johan Commelin (Oct 28 2020 at 13:29):
Thanks! With some help from Anne I managed to make it work
Last updated: May 09 2021 at 21:10 UTC