Macro for generating struct fields?

Stream: lean4

[Phil Nguyen]

Hi! I have a basic macro question.

I'd like to generate a structure whose fields are computed from some static arguments. In this minimal example, I attempt to generate fields from passed in names, all typed String:

macro "structure_with_fields " name:ident fields:ident* : command => do
  let mut decl ← `(structure $name where)
  for f in fields do
    decl ← `(command| $decl ($f : String))
  return decl

But I'm getting an error after the $decl, saying "unexpected token (".

Some questions:

• How can I generate the structure in this example?
• Do structure's field declarations have their own declared syntax category?

Many thanks!!

[Robin Arnez]

The fields are part of the structure command and not something after the command so you need to put in the quotation containing the structure token:

macro "structure_with_fields " name:ident fields:ident* : command => do
  `(structure $name where $[($fields:ident : String)]*)

[Phil Nguyen]

I see. Thank you so much!!