Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: mk_app fails to retrieve declaration


view this post on Zulip Patrick Massot (Dec 20 2020 at 21:39):

What am I doing wrong in:

import tactic

namespace tactic.interactive

setup_tactic_parser

open tactic

meta def test (i : parse ident) (args : parse pexpr_list_or_texpr) : tactic unit :=
do
  eargs  args.mmap tactic.to_expr,
  tactic.mk_app i eargs >>= tactic.exact

end tactic.interactive

set_option trace.app_builder true

example (a : ) (h :  n : , true) : true :=
begin
  test h [a],
end

view this post on Zulip Patrick Massot (Dec 20 2020 at 21:47):

@Mario Carneiro?

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:48):

mk_app expects the name of a constant in the first argument, it doesn't work on local constants

view this post on Zulip Patrick Massot (Dec 20 2020 at 21:48):

Is there any function I could use here?

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:48):

yes, I forget the name

view this post on Zulip Patrick Massot (Dec 20 2020 at 21:48):

I'd like something that can handle both local constants and lemma names.

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:49):

the function I'm thinking of takes an expr in the first position

view this post on Zulip Patrick Massot (Dec 20 2020 at 21:49):

Indeed my code works if I create a lemma replacing h

view this post on Zulip Mario Carneiro (Dec 20 2020 at 21:49):

so you can use general expressions in addition to local constants

view this post on Zulip Patrick Massot (Dec 20 2020 at 21:49):

Great

view this post on Zulip Patrick Massot (Dec 20 2020 at 21:49):

How do we find it?

view this post on Zulip Jannis Limperg (Dec 20 2020 at 22:07):

expr.mk_app perchance?

view this post on Zulip Patrick Massot (Dec 20 2020 at 22:11):

Jannis, could you try to fix my code using that function?

view this post on Zulip Patrick Massot (Dec 20 2020 at 22:11):

I failed so far.

view this post on Zulip Patrick Massot (Dec 20 2020 at 22:13):

Nevermind, this is a parsing issue

view this post on Zulip Patrick Massot (Dec 20 2020 at 22:13):

Thank you very much.

view this post on Zulip Mario Carneiro (Dec 20 2020 at 22:17):

yeah, I was thinking of expr.mk_app but it's not a particularly good drop in replacement for mk_app because it doesn't do implicit stuff

view this post on Zulip Patrick Massot (Dec 20 2020 at 22:20):

I need to go to bed, but I'd be very happy to read a more robust solution when I'll wake up.


Last updated: May 09 2021 at 23:10 UTC