chore: restore example after stage0 update (#6942)

leanprover · Feb 4, 2025 · 63ac27e · 63ac27e
1 parent 897e9c5
commit 63ac27e
Showing 1 changed file with 3 additions and 4 deletions.
diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean
@@ -350,10 +350,9 @@ def SemanticTokenType.toNat (tokenType : SemanticTokenType) : Nat :=
   tokenType.toCtorIdx
 
 -- sanity check
--- TODO: restore after update-stage0
---example {v : SemanticTokenType} : open SemanticTokenType in
---    names[v.toNat]?.map (toString <| toJson ·) = some (toString <| toJson v) := by
---  cases v <;> native_decide
+example {v : SemanticTokenType} : open SemanticTokenType in
+    names[v.toNat]?.map (toString <| toJson ·) = some (toString <| toJson v) := by
+  cases v <;> native_decide
 
 /--
 The semantic token modifiers included by default in the LSP specification.