quoting a ctor

Stream: lean4

[Adam Topaz]

I'd like to make a macro that constructs an inductive type with n elements, but I can't seem to figure out how to write the syntax for the constructor. The underscore in the following is what I'd like to fill in... what am I missing?

import Lean

open Lean

def mkIdents (i : Name) (n : Nat) : Array Ident :=
  List.range n |>.toArray |>.map fun n => mkIdent <| s!"{i}{n}"

macro "test" : command => do
  let idents := mkIdents `x 3
  `(inductive foo where $[$(← idents.mapM fun i => _)]*)

[Mario Carneiro]

does

macro "test" : command => do
  let idents := mkIdents `x 3
  `(inductive foo where $[| $idents:ident]*)

count?

[Adam Topaz]

Ah great. I did try this out before but without the :ident, and it did not work. But that's good enough for me. Thanks Mario!

[Adam Topaz]

I would still be interested in seeing how to make the original code work (the one with mapM), if it's possible. Just for my own understanding.

[Mario Carneiro]

`(Lean.Parser.Command.ctor| | $i:ident) works in that position

[Adam Topaz]

I see. Thanks again! I didn't know that I can just put the parser name in the quotation like that.

[Mario Carneiro]

if you don't specify the name it defaults to term (also overloaded with one for command), which is often not what you want

[Mario Carneiro]

it doesn't use type information because the choice of parser affects the parsing of the rest of the quotation

[Adam Topaz]

yes I am aware of that. But I was under the impression that to be able to write (term| ...) or (command| ...) or (tactic| ...) there was some other step under the hood. I naively tried (ctor| ...) which didn't work, so that's why I came to zulip :)

[Mario Carneiro]

parser categories don't need to be namespaced, but other parsers do

[Adam Topaz]

I understand now. Thanks again Mario. that was very helpful.