What is SyntaxKind?

Stream: lean4

[Kevin Cheung]

In the Elaboration chapter of Metaprogramming in Lean 4, SyntaxKind is mentioned. But I couldn't seem to find its definition. What would be an intuitive way to understand SyntaxKind?

[Damiano Testa]

Do you mean a docs#Lean.SyntaxNodeKind, maybe?

[Kevin Cheung]

I don't know. Here is the paragraph in the book:

In the following example, we are not extending the original #check syntax, but adding a new SyntaxKind for this specific syntax construct. However, from the point of view of the user, the effect is basically the same.

[Kevin Cheung]

The only other mention in the book is in the following paragraph:

2. If no macro can be applied, we search for all CommandElabs that have been registered for the SyntaxKind of the Syntax we are elaborating, using the command_elab attribute.

[Damiano Testa]

I am not completely sure what a SyntaxKind really is, but this is what the syntax tree for #check "mycheck" (from the book) looks like before and after adding the new elab:

/-
node Lean.Parser.Command.check, none
|-atom original: ⟨⟩⟨ ⟩-- '#check'
|-node str, none
|   |-atom original: ⟨⟩⟨⏎⏎⟩-- '"mycheck"'
-/
#check "mycheck"

elab "#check" "mycheck" : command => do
  Lean.logInfo "Got ya!"

/-
node «command#checkMycheck», none
|-atom original: ⟨⟩⟨ ⟩-- '#check'
|-atom original: ⟨⟩⟨⏎⏎⟩-- 'mycheck'
-/
#check mycheck

[Damiano Testa]

Next to node you see the SyntaxNodeKind which typically gives you information on what parser has "read" the corresponding node. As you can see, the first one, has been read by the "usual" check parser. After the elab, though, the parsing has been taken over by the newly defined elaborator and the SyntaxNodeKind is indeed the new one.

[Kevin Cheung]

I see. I guess SyntaxKind is probably just a typo for SyntaxNodeKind. Thank you.