chore(library/init/lean/syntax): simplify SyntaxNodeKind

library/init/lean/parser/parser.lean

@@ -458,8 +458,8 @@ def quotedCharFn : BasicParserFn
     else
       s.mkError "invalid escape sequence"
 
-def strLitKind : SyntaxNodeKind := { name := `strLit }
-def numLitKind : SyntaxNodeKind := { name := `numLit }
+def strLitKind : SyntaxNodeKind := `strLit
+def numLitKind : SyntaxNodeKind := `numLit
 
 /-- Push `(Syntax.node tk <new-atom>)` into syntax stack -/
 def mkNodeToken (n : SyntaxNodeKind) (startPos : Nat) : BasicParserFn :=
@@ -895,7 +895,7 @@ let find (n : Name) : ParserState × List α :=
 match stx with
 | some (Syntax.atom _ sym)      := find (mkSimpleName sym)
 | some (Syntax.ident _ _ _ _ _) := find `ident
-| some (Syntax.node k _ _)      := find k.name
+| some (Syntax.node k _ _)      := find k
 | _                             := (s, [])
 
 private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=

library/init/lean/syntax.lean

@@ -29,14 +29,10 @@ def SourceInfo.updateTrailing : SourceInfo → Substring → SourceInfo
 
 /- Node kind generation -/
 
-structure SyntaxNodeKind :=
-(name : Name)
+abbrev SyntaxNodeKind := Name
 
-instance stxKindBeq : HasBeq SyntaxNodeKind :=
-⟨λ k₁ k₂, k₁.name == k₂.name⟩
-
-@[pattern] def choiceKind : SyntaxNodeKind := ⟨`choice⟩
-@[pattern] def nullKind : SyntaxNodeKind := ⟨`null⟩
+@[pattern] def choiceKind : SyntaxNodeKind := `choice
+@[pattern] def nullKind : SyntaxNodeKind := `null
 
 /- Syntax AST -/
 
@@ -203,10 +199,10 @@ protected partial def formatStx : Syntax → Format
   format "`" ++ format val ++ scopes
 | (node kind args scopes) :=
   let scopes := match scopes with [] := format "" | _ := bracket "{" (joinSep scopes.reverse ", ") "}" in
-  if kind.name = `Lean.Parser.noKind then
+  if kind = `Lean.Parser.noKind then
     sbracket $ scopes ++ joinSep (args.toList.map formatStx) line
   else
-    let shorterName := kind.name.replacePrefix `Lean.Parser Name.anonymous in
+    let shorterName := kind.replacePrefix `Lean.Parser Name.anonymous in
     paren $ joinSep ((format shorterName ++ scopes) :: args.toList.map formatStx) line
 | missing := "<missing>"
 

tests/playground/parser1.lean

@@ -5,15 +5,15 @@ open Lean.Parser
 local infixl `>>`:50 := Lean.Parser.andthen
 
 @[builtinTestParser] def pairParser : Parser :=
-node ⟨`pairKind⟩ $
+node `pairKind $
   "(" >> numLit >> "," >> ident >> ")"
 
 @[builtinTestParser] def pairsParser : Parser :=
-node ⟨`pairsKind⟩ $
+node `pairsKind $
   "{" >> sepBy1 testParser "," >> "}"
 
 @[builtinTestParser] def functionParser : Parser :=
-node ⟨`funKind⟩ $
+node `funKind $
   "fun" >> ident >> "," >> testParser
 
 @[builtinTestParser] def identParser : Parser :=