max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove confusing comment

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-11 11:03:18 +02:00 • committed by Leonardo de Moura
parent 7a7a14c8b9
commit d33b5a8ea6
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Data/JsonRpc.lean
View file

@ -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)