Pattern matching optional `Syntax`

Stream: metaprogramming / tactics

[Eric Wieser]

What am I doing wrong here?

syntax:max (name := fin_eta) "fin_eta% " term:max term:max (term)? : term

@[term_elab fin_eta]
def Elab : Lean.Elab.Term.TermElab
| `($mStx:term $nStx:term $[$A:term]?), expectedType? =>
  sorry

The $[$A:term]? syntax is apparently wrong but I don't know how to search for the correct syntax

[Eric Wieser]

(As far as I can tell I can't use the simpler elab because then I don't get to make my own decision about postponing)

[Alex Keizer]

Can you avoid the match entirely, and just access the different parts by indexing?

[Eric Wieser]

Sure, but that's way uglier

[Kyle Miller]

In a PM we discovered it was that the pattern was missing fin_eta% at the beginning.