mk_app fails to retrieve declaration

Stream: metaprogramming / tactics

[Patrick Massot]

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

[Patrick Massot]

@Mario Carneiro?

[Mario Carneiro]

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

[Patrick Massot]

Is there any function I could use here?

[Mario Carneiro]

yes, I forget the name

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

Indeed my code works if I create a lemma replacing h

[Mario Carneiro]

so you can use general expressions in addition to local constants

[Patrick Massot]

Great

[Patrick Massot]

How do we find it?

[Jannis Limperg]

expr.mk_app perchance?

[Patrick Massot]

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

[Patrick Massot]

I failed so far.

[Patrick Massot]

Nevermind, this is a parsing issue

[Patrick Massot]

Thank you very much.

[Mario Carneiro]

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]

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