chore: add sanity check for SemanticTokenType/Modifier.names

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -252,6 +252,7 @@ inductive SemanticTokenType where
   | regexp
   | operator
   | decorator
+  deriving ToJson, FromJson
 
 -- must be in the same order as the constructors
 def SemanticTokenType.names : Array String :=
@@ -263,6 +264,11 @@ def SemanticTokenType.names : Array String :=
 def SemanticTokenType.toNat (type : SemanticTokenType) : Nat :=
   type.toCtorIdx
 
+-- sanity check
+theorem SemanticTokenType.names_toNat_eq_toJson {v : SemanticTokenType} :
+names[v.toNat]?.map (toString <| toJson ·) = some (toString <| toJson v) := by
+  cases v <;> (dsimp only [toNat, toCtorIdx, names]; native_decide)
+
 /--
 The semantic token modifiers included by default in the LSP specification.
 Not used by the Lean core, but implementing them here allows them to be
@@ -279,15 +285,21 @@ inductive SemanticTokenModifier where
   | modification
   | documentation
   | defaultLibrary
+  deriving ToJson, FromJson
 
 -- must be in the same order as the constructors
 def SemanticTokenModifier.names : Array String :=
   #["declaration", "definition", "readonly", "static", "deprecated", "abstract",
     "async", "modification", "documentation", "defaultLibrary"]
 
-def SemanticTokenModifier.toNat (modifier : SemanticTokenType) : Nat :=
+def SemanticTokenModifier.toNat (modifier : SemanticTokenModifier) : Nat :=
   modifier.toCtorIdx
 
+-- sanity check
+theorem SemanticTokenModifier.names_toNat_eq_toJson {v : SemanticTokenModifier} :
+names[v.toNat]?.map (toString <| toJson ·) = some (toString <| toJson v) := by
+  cases v <;> (dsimp only [toNat, toCtorIdx, names]; native_decide)
+
 structure SemanticTokensLegend where
   tokenTypes : Array String
   tokenModifiers : Array String