From 434564b125808c8b50dbd970eb4e5b9334bbc96f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 28 Jan 2021 15:51:47 +0100 Subject: [PATCH] chore: clean up manual From/ToJson instances --- src/Lean/Data/Lsp/LanguageFeatures.lean | 32 ++++--------------------- 1 file changed, 4 insertions(+), 28 deletions(-) diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index 9705471adb..c48d3b0fa3 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -20,40 +20,16 @@ structure Hover where deriving ToJson, FromJson structure HoverParams extends TextDocumentPositionParams - -instance : FromJson HoverParams := ⟨fun j => do - let tdpp ← @fromJson? TextDocumentPositionParams _ j - pure ⟨tdpp⟩⟩ - -instance : ToJson HoverParams := - ⟨fun o => toJson o.toTextDocumentPositionParams⟩ + deriving FromJson, ToJson structure DeclarationParams extends TextDocumentPositionParams - -instance : FromJson DeclarationParams := ⟨fun j => do - let tdpp ← @fromJson? TextDocumentPositionParams _ j - pure ⟨tdpp⟩⟩ - -instance : ToJson DeclarationParams := - ⟨fun o => toJson o.toTextDocumentPositionParams⟩ + deriving FromJson, ToJson structure DefinitionParams extends TextDocumentPositionParams - -instance : FromJson DefinitionParams := ⟨fun j => do - let tdpp ← @fromJson? TextDocumentPositionParams _ j - pure ⟨tdpp⟩⟩ - -instance : ToJson DefinitionParams := - ⟨fun o => toJson o.toTextDocumentPositionParams⟩ + deriving FromJson, ToJson structure TypeDefinitionParams extends TextDocumentPositionParams - -instance : FromJson TypeDefinitionParams := ⟨fun j => do - let tdpp ← @fromJson? TextDocumentPositionParams _ j - pure ⟨tdpp⟩⟩ - -instance : ToJson TypeDefinitionParams := - ⟨fun o => toJson o.toTextDocumentPositionParams⟩ + deriving FromJson, ToJson structure DocumentSymbolParams where textDocument : TextDocumentIdentifier