'failed to infer binder type' error

Stream: lean4

[Juneyoung Lee]

Hi all, I defined a toy tactic and used it as follows:

macro "add_true" h:ident: tactic =>
  `(tactic|
      have ($h:ident): True := True.intro
    )

example: True := by
  add_true h_new
  sorry

However, it shows an error message at h_new as follows:

failed to infer binder type

h_new: ?m.4780

Any idea how this can be resolved?

[Damiano Testa]

This works:

import Std
open Lean Elab Tactic

elab "add_true" h:ident : tactic => do
  evalTactic (← `(tactic| have $h:ident: True := True.intro ))

example: True := by
  add_true h_new
  sorry

[Jannis Limperg]

I think the parentheses around $h:ident make it into a pattern and then Lean gets confused. Without the parentheses, it works:

macro "add_true" h:ident: tactic =>
  `(tactic|
      have $h:ident : True := True.intro
    )

example: True := by
  add_true h_new