match with `("&" foo)*` syntax

Stream: new members

[Edward van de Meent]

i've defined some custom syntax, and i'd like to define an elaborator for this. however, i can't seem to find a way to match with it...

import Lean

open Lean Elab Term

declare_syntax_cat foo
syntax "foo_term" : foo

declare_syntax_cat bar
syntax "bar_term" : bar

syntax foo ("&" bar)* : term

def customElab : TermElab := fun z _ => match z with
  -- `($f:foo ??????) => success -- i have no clue how to make this work
  | _ => throwUnsupportedSyntax

looking at #fpil and metaprogramming, the only related idea i could find is matching with syntax defined like bar,*, but that doesn't work here sadly. i also came across $[...], but i'm not sure if it's applicable, because i haven't found a good example of what that does.

[Edward van de Meent]

nvm i figured it out; the right way to match this is `($f:foo $[& $b:bar]*)

[Edward van de Meent]

as a sidenote: today i realized that syntax term ("&" term)* : term and similar constructions are a quick way to make the server stack overflow, because of ambiguous interpretations and non-tail recursion. (i.e. when trying to parse a term, it sees this new rule and thinks "ah, maybe i need to find a term first" and starts the whole search again, just to come across this rule again, etc.)