Unknown identifier in custom tactic

Stream: new members

[Matei Mandache]

Hi, I'm having trouble with using some of my custom-built tactics. Here's a mwe:

meta def my_skip (n : ℕ) : tactic unit := skip

theorem foo (n : ℕ) : n = n :=
begin
  my_skip n,
  refl,
end

lean complains that n is an unknown identifier in my_skip n, which seems a bit strange. Does anyone know why this is happening and how it can be fixed? Many thanks!

[Yakov Pechersky]

It needs to be in the right namespace. "meta def tactic.interactive.my_skip"

[Alex J. Best]

I think my_skip needs to be in the tactic.interactive namespace

[Matei Mandache]

Like this?

meta def tactic.interactive.my_skip (n : ℕ) : tactic unit := skip

theorem foo (n : ℕ) : n = n :=
begin
  my_skip n,
  refl,
end

It's still coming up with the error

[Johan Commelin]

I don't think tactic.interactive was the issue. Because the initial error didn't complain that my_skip was unknown.

[Johan Commelin]

But I might just be waffling. I don't really know the inner workings of the tactic framework

[Kevin Buzzard]

An interactive tactic doesn't look like that, I don't think; it has to have some parser etc.

[Kevin Buzzard]

My memory is that after := you need something like `[skip] or something, but this is all explained in the tactic writing tutorial and videos

[Kevin Buzzard]

meta def my_skip : tactic unit := tactic.interactive.skip seems to work fine

[Kevin Buzzard]

But if you want the n then you're going to have to parse it, and figure out the differences between names, exprs, pexprs etc I guess

[Scott Morrison]

e.g.

import tactic

open tactic

setup_tactic_parser
meta def tactic.interactive.my_skip (n : parse texpr) : tactic unit :=
do
  trace n,
  skip

theorem foo (n : ℕ) : n = n :=
begin
  my_skip n,
  refl,
end

[Scott Morrison]

Please watch Rob's videos on metaprogramming!