Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: apply name


view this post on Zulip 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`

view this post on Zulip Jannis Limperg (Oct 28 2020 at 12:54):

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

view this post on Zulip 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