Command for making structures

Stream: lean4

[Adam Topaz]

I'm trying to figure out how to make a command that creates a structure where the number of fields can vary.
For instance,

macro "test" s:declId : command => `(structure $s where)

would give me a command where test foo would make an empty structure called foo.

Now what I want similar command, but with an additional parameter, say n, e.g.

macro "test" s:declId n:num : command => sorry

For simplicity, let's just say that this command should create a structure named $s, with n fields, say called a_1, a_2, ..., a_n, all of type Nat.

I'm not really sure where to even look for examples of such things. Can anyone point me in the right direction?

[Marcus Rossel]

This works:

import Lean
open Lean

macro "test" s:declId n:num : command => do
  let mut idents : Array Ident := #[]
  for idx in [:n.getNat] do
    idents := idents.push (mkIdent s!"a_{idx}")
  `(structure $s where $[$idents:ident : Nat]*)

[Marcus Rossel]

I think the main challenge is the splice, about which I've had a question recently.

[Adam Topaz]

Thanks! This is much easier than I expected!

[Adam Topaz]

BTW, is there somewhere where I can read more about $[ ... ]*?