using another tactic inside a meta function

Stream: metaprogramming / tactics

[Ayush Agrawal]

I am trying to understand how tactic writing is done in Lean. I have a very trivial doubt here:
simple use of intro

example : ∀ (x : ℕ ), ∀ e > 0, ∃ n : ℕ, x < n*e :=
begin
  intro c,
end

successfully generates a tactic state : image.png

But when I call tactic.intro inside a meta function like this :

meta def intro_copy (q : name) : tactic expr :=
do
  tactic.intro q

and use intro_copy c inside begin end block, it is showing unknown identifier c . I am not understanding what should be the appropriate way to do this and what should be the general approach in using other tactics inside a meta function while writing tactics. Any leads on this @Mario Carneiro ?

[Mario Carneiro]

The issue is that you are calling a noninteractive tactic in a tactic block, so you don't get any parsing niceties. You would have to write intro_copy `c since that's the syntax to pass a name to a function

[Mario Carneiro]

If you want to use a tactic parser, then you need to put intro_copy in the tactic.interactive namespace, and use parse ident as the type of q, similar to what src#tactic.interactive.intro is doing

[Ayush Agrawal]

Thanks @Mario Carneiro it did work! implementation of intro is in two files as I saw : interactive.lean and tactic.lean: are these implementation meant to be interdependent or are used for different purposes?

[Mario Carneiro]

the first one is the interactive tactic, the second is the noninteractive tactic

[Mario Carneiro]

the interactive tactic has a special type signature using parse which indicates how the tactic is parsed

[Mario Carneiro]

otherwise it is just a wrapper for the noninteractive tactic in most cases

[Mario Carneiro]

generally, the interactive tactic is meant to be called by users by a begin-end block, and the noninteractive tactic is meant to be called by other tactics in a do block / metaprogramming contexts