syntax keyword

Stream: new members

[Xiyu Zhai]

Hi, all. I wonder what the following means:

/-- A `bigOpBinder` is like an `extBinder` and has the form `x`, `x : ty`, or `x pred`
where `pred` is a `binderPred` like `< 2`.
Unlike `extBinder`, `x` is a term. -/
syntax bigOpBinder := term:max ((" : " term) <|> binderPred)?

Is it the same as:

syntax (name := bigOpBinder) term:max ((" : " term) <|> binderPred)?

ChatGPT told me they are different and in the first, "The bigOpBinder is a distinct syntax category, like a shorthand for the specific structure described."

However, by hovering over the type of bigOpBinder, it seems that ChatGPT is wrong and I'm correct. It's interesting because Claude agrees with ChatGPT.

I couldn't find relevant reference in the documentation for now.

[Kyle Miller]

The second one is syntactically invalid, unless I'm missing something (note the red squiggle at the end of the line)

[Edward van de Meent]

i suspect it's missing : term at the end

[Kyle Miller]

That would be incorrect though, since bigOpBinder is not supposed to be a term.

[Edward van de Meent]

so it is its own syntax category then?

[Edward van de Meent]

answer : no

[Kyle Miller]

No, a syntax category is its own thing. Let's say we did add : term to the second one to make something that's syntactically correct (even though that would logically be incorrect), both would define a new syntax kind, and the second would add that to the term category.

[Edward van de Meent]

i was under the impression that every defined syntax has to be part of some category... is that wrong then?

[Kyle Miller]

Yes

[Edward van de Meent]

then every syntax is either its own syntaxkind or is part of a syntax category?

[Kyle Miller]

No, being part of a syntax category is independent. But as far as I know every syntax does create a parser that wraps its result in a Syntax.node with a unique kind (specified by the LHS of the := in a syntax abbreviation, or by the (name := ...) in the second form. If the (name := ...) is omitted, then the name is auto-generated.)

[Kyle Miller]

If you are using the lower-level parsers (via def rather than this higher-level syntax), then you can create syntax abbreviations that don't insert such a Syntax.node.

[Xiyu Zhai]

Thanks a lot!