From d33b5a8ea6dfa7d0451846b884898d1fffe0e2fd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 11 Aug 2020 11:03:18 +0200 Subject: [PATCH] chore: remove confusing comment --- src/Lean/Data/JsonRpc.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index da129fe4ba..99f0aa8e76 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -67,9 +67,7 @@ instance ErrorCode.hasToJson : HasToJson ErrorCode := | ErrorCode.requestCancelled => (-32800 : Int) | ErrorCode.contentModified => (-32801 : Int)⟩ -/- Uses Option Structured because users will likely rarely distinguish between an empty -parameter array and an omitted params field. -Uses separate constructors for notifications and errors because client and server +/- Uses separate constructors for notifications and errors because client and server behavior is expected to be wildly different for both. -/ inductive Message | request (id : RequestID) (method : String) (params? : Option Structured)