macro with sequence of arguments

Stream: lean4

[Calle Sönne]

I am trying to write a macro for another tactic, which takes in an unspecified length sequence of arguments. I have tried to implement it as follows:

/-- Version of `algebraize`, which only adds `Algebra` instances and `IsScalarTower` instances. -/
macro "algebraize'" t:term:max+ : tactic =>
  `(tactic| algebraize (config := {searchContext := false}) $t*)

So this macro just calls this algebraize tactic with a specific config. My issue is with t:term:max+, as this will try to interpret the tactic on the next line as an argument. How do I avoid this? I want to use colGt somehow, but if I try for example t:(colGt term:max)+ then the substitution $t* on the next line fails.

I have been able to do this by splitting it up into two parts as follows:

syntax "algebraize'" (ppSpace colGt term:max)* : tactic

/-- Version of `algebraize`, which only adds `Algebra` instances and `IsScalarTower` instances. -/
macro_rules
  | `(tactic| algebraize' $[$t:term]*) =>
    `(tactic| algebraize (config := {searchContext := false}) $t*)

But I feel that with such a simple macro, I should be able to do it in one line. Does anyone know how to do this?

[Jon Eugster]

(the related PR is #16217)

I don't exactly know the details, but it looks like

macro "algebraize'" t:(colGt term:max)* : tactic =>
  `(tactic| algebraize (config := {searchContext := false}) $[$t]* )

works when I try it

[Calle Sönne]

Jon Eugster said:

(the related PR is #16217)

I don't exactly know the details, but it looks like

macro "algebraize'" t:(colGt term:max)* : tactic =>
  `(tactic| algebraize (config := {searchContext := false}) $[$t]* )

works when I try it

Thanks! I don't fully understand what the syntax for "substituting" these TSyntax objects is yet.