Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: using another tactic inside a meta function


Ayush Agrawal (Oct 17 2021 at 16:23):

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 (Oct 17 2021 at 16:25):

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 (Oct 17 2021 at 16:27):

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 (Oct 17 2021 at 17:25):

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 (Oct 17 2021 at 17:26):

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

Mario Carneiro (Oct 17 2021 at 17:26):

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

Mario Carneiro (Oct 17 2021 at 17:26):

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

Mario Carneiro (Oct 17 2021 at 17:28):

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


Last updated: Dec 20 2023 at 11:08 UTC