`elab_rules : tactic` patterns require redundant information

[leodemoura]

import Lean

syntax "foo " str : tactic

open Lean Elab
elab_rules : tactic
  | `(foo $x:str) => logInfo x.getString

example : True := by
 foo "hello"  -- Error `tacticFoo_` has not been implemented

One has to write the elab_rules above as

elab_rules : tactic
  | `(tactic| foo $x:str) => logInfo x.getString

[Vtec234]

I just ran into this as well. I think Tactic should be TSyntax `tactic -> TacticM Unit rather than Syntax -> TacticM Unit.

[Kha]

@Vtec234 It should, but in order to generate a type error here we would also have to fix Macro as mentioned in https://github.com/leanprover/lean4/pull/1251