syntax with optional suffix

Stream: metaprogramming / tactics

[nnarek]

I am expecting that sum and sum_ should match with iaggr_sum, but it does not, and I do not understand why.
Instead of such syntax, I can add sum_ Sum_ SUM_ ... symbols too, but I want to write short code

import Lean
open Lean

declare_syntax_cat iaggr_sum
syntax (name := iaggr_sum) ("sum" <|> "Sum" <|> "SUM"
       <|> "summation" <|> "Summation" <|> "SUMMATION") (noWs "_")? : iaggr_sum

syntax "test(" iaggr_sum ")" : term

elab "test(" t:iaggr_sum ")" : term => pure $ mkStrLit (toString t)

#check test( sum )
#check test( sum_ )

[Aaron Liu]

sum_ is a valid identifier

[nnarek]

sorry, not sure that I correctly understood you. Do you mean that sum_ gets parsed as ident?
can you please explain why sum_ does not match with syntax of iaggr_sum and what I can do to fix it

[Aaron Liu]

sum_ gets parsed as an ident

[Aaron Liu]

I don't think you can "fix" it

[nnarek]

But it does not explain why sum is not parsed via parser of ident. Are there any doc that explain how parsers are picked and how they are prioritized against each other?

[Aaron Liu]

sum is a token, so it is invalid as an ident

[nnarek]

Thank you