Trouble with antiquotations

Stream: lean4

[Eric Wieser]

The following isn't working, and I can't work out how to find documentation on the particular order of $ and [ symbols needed to match the syntax I want:

import Lean

open Lean

syntax "foo: " sepBy1("bar"? term,", ") : term

macro_rules
| `(foo: $[bar?%$bars $ts],*) => do
    `($(Lean.Quote.quote ts.size))

syntax "foo2: " withPosition(group(colGe term ","?)*) : term

-- like `foo` but doesn't support `bar`
macro_rules
| `(foo2: $[ $ts $[,]? ]*) => `(foo: $[$ts],*)

#check foo: bar 1, 2, bar 3
#check foo: 1, 1, 2
#check foo2: 2, 2

[Eric Wieser]

Is there a cheat sheet somewhere that translates between macro-macros like sepByOne(, the declarations like sepByOne, and the antiquotation syntax needed to match against them?

[Shreyas Srinivas]

Some documentation on parsers, syntax, quotations, and anti-quotations would be really helpful in general. Currently we have the metaprogramming book, the Lean.Parser doc page, and examples from Mathlib and zulip, and @Arthur Paulino 's Fxy language project. It sounds like a lot but this is really not much to go on