Stream: metaprogramming / tactics

Topic: mk_app fails to retrieve declaration

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


@Mario Carneiro?

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

Patrick Massot (Dec 20 2020 at 21:48):

Is there any function I could use here?

Mario Carneiro (Dec 20 2020 at 21:48):

yes, I forget the name

Patrick Massot (Dec 20 2020 at 21:48):

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

Mario Carneiro (Dec 20 2020 at 21:49):

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

Patrick Massot (Dec 20 2020 at 21:49):

Indeed my code works if I create a lemma replacing h

Mario Carneiro (Dec 20 2020 at 21:49):

so you can use general expressions in addition to local constants

Great

Patrick Massot (Dec 20 2020 at 21:49):

How do we find it?

Jannis Limperg (Dec 20 2020 at 22:07):

expr.mk_app perchance?

Patrick Massot (Dec 20 2020 at 22:11):

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

I failed so far.

Patrick Massot (Dec 20 2020 at 22:13):

Nevermind, this is a parsing issue

Patrick Massot (Dec 20 2020 at 22:13):

Thank you very much.

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

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