inductive Lapis.Protocol.JsonRpc.RequestId : Type

• num (n : Int) : RequestId
• str (s : String) : RequestId

instance Lapis.Protocol.JsonRpc.instInhabitedRequestId : Inhabited RequestId

Equations

• Lapis.Protocol.JsonRpc.instInhabitedRequestId = { default := Lapis.Protocol.JsonRpc.instInhabitedRequestId.default }

def Lapis.Protocol.JsonRpc.instInhabitedRequestId.default : RequestId

Equations

• Lapis.Protocol.JsonRpc.instInhabitedRequestId.default = Lapis.Protocol.JsonRpc.RequestId.num default

instance Lapis.Protocol.JsonRpc.instBEqRequestId : BEq RequestId

Equations

• Lapis.Protocol.JsonRpc.instBEqRequestId = { beq := Lapis.Protocol.JsonRpc.instBEqRequestId.beq }

def Lapis.Protocol.JsonRpc.instBEqRequestId.beq : RequestId → RequestId → Bool

Equations

• Lapis.Protocol.JsonRpc.instBEqRequestId.beq (Lapis.Protocol.JsonRpc.RequestId.num a) (Lapis.Protocol.JsonRpc.RequestId.num b) = (a == b)
• Lapis.Protocol.JsonRpc.instBEqRequestId.beq (Lapis.Protocol.JsonRpc.RequestId.str a) (Lapis.Protocol.JsonRpc.RequestId.str b) = (a == b)
• Lapis.Protocol.JsonRpc.instBEqRequestId.beq x✝¹ x✝ = false

instance Lapis.Protocol.JsonRpc.instHashableRequestId : Hashable RequestId

Equations

• Lapis.Protocol.JsonRpc.instHashableRequestId = { hash := Lapis.Protocol.JsonRpc.instHashableRequestId.hash }

def Lapis.Protocol.JsonRpc.instHashableRequestId.hash : RequestId → UInt64

Equations

• Lapis.Protocol.JsonRpc.instHashableRequestId.hash (Lapis.Protocol.JsonRpc.RequestId.num a) = mixHash 0 (hash a)
• Lapis.Protocol.JsonRpc.instHashableRequestId.hash (Lapis.Protocol.JsonRpc.RequestId.str a) = mixHash 1 (hash a)

instance Lapis.Protocol.JsonRpc.instReprRequestId : Repr RequestId

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instToJsonRequestId : Lean.ToJson RequestId

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instFromJsonRequestId : Lean.FromJson RequestId

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instToStringRequestId : ToString RequestId

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Protocol.JsonRpc.parseError : Int

JSON-RPC 2.0 error codes

Equations

• Lapis.Protocol.JsonRpc.parseError = -32700

def Lapis.Protocol.JsonRpc.invalidRequest : Int

Equations

• Lapis.Protocol.JsonRpc.invalidRequest = -32600

def Lapis.Protocol.JsonRpc.methodNotFound : Int

Equations

• Lapis.Protocol.JsonRpc.methodNotFound = -32601

def Lapis.Protocol.JsonRpc.invalidParams : Int

Equations

• Lapis.Protocol.JsonRpc.invalidParams = -32602

def Lapis.Protocol.JsonRpc.internalError : Int

Equations

• Lapis.Protocol.JsonRpc.internalError = -32603

def Lapis.Protocol.JsonRpc.serverNotInitialized : Int

Equations

• Lapis.Protocol.JsonRpc.serverNotInitialized = -32002

def Lapis.Protocol.JsonRpc.unknownErrorCode : Int

Equations

• Lapis.Protocol.JsonRpc.unknownErrorCode = -32001

def Lapis.Protocol.JsonRpc.requestCancelled : Int

Equations

• Lapis.Protocol.JsonRpc.requestCancelled = -32800

def Lapis.Protocol.JsonRpc.contentModified : Int

Equations

• Lapis.Protocol.JsonRpc.contentModified = -32801

structure Lapis.Protocol.JsonRpc.ResponseError : Type

• code : Int
• message : String
• data : Option Lean.Json

def Lapis.Protocol.JsonRpc.instInhabitedResponseError.default : ResponseError

Equations

• Lapis.Protocol.JsonRpc.instInhabitedResponseError.default = { code := default, message := default, data := default }

instance Lapis.Protocol.JsonRpc.instInhabitedResponseError : Inhabited ResponseError

Equations

• Lapis.Protocol.JsonRpc.instInhabitedResponseError = { default := Lapis.Protocol.JsonRpc.instInhabitedResponseError.default }

instance Lapis.Protocol.JsonRpc.instReprResponseError : Repr ResponseError

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instToJsonResponseError : Lean.ToJson ResponseError

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instFromJsonResponseError : Lean.FromJson ResponseError

Equations

• One or more equations did not get rendered due to their size.

structure Lapis.Protocol.JsonRpc.RequestMessage : Type

A JSON-RPC 2.0 request message

• id : RequestId
• method : String
• params : Option Lean.Json

instance Lapis.Protocol.JsonRpc.instInhabitedRequestMessage : Inhabited RequestMessage

Equations

• Lapis.Protocol.JsonRpc.instInhabitedRequestMessage = { default := Lapis.Protocol.JsonRpc.instInhabitedRequestMessage.default }

def Lapis.Protocol.JsonRpc.instInhabitedRequestMessage.default : RequestMessage

Equations

• Lapis.Protocol.JsonRpc.instInhabitedRequestMessage.default = { id := default, method := default, params := default }

instance Lapis.Protocol.JsonRpc.instReprRequestMessage : Repr RequestMessage

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instToJsonRequestMessage : Lean.ToJson RequestMessage

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instFromJsonRequestMessage : Lean.FromJson RequestMessage

Equations

• One or more equations did not get rendered due to their size.

structure Lapis.Protocol.JsonRpc.NotificationMessage : Type

A JSON-RPC 2.0 notification message (no id, no response expected)

• method : String
• params : Option Lean.Json

def Lapis.Protocol.JsonRpc.instInhabitedNotificationMessage.default : NotificationMessage

Equations

• Lapis.Protocol.JsonRpc.instInhabitedNotificationMessage.default = { method := default, params := default }

instance Lapis.Protocol.JsonRpc.instInhabitedNotificationMessage : Inhabited NotificationMessage

Equations

• Lapis.Protocol.JsonRpc.instInhabitedNotificationMessage = { default := Lapis.Protocol.JsonRpc.instInhabitedNotificationMessage.default }

instance Lapis.Protocol.JsonRpc.instReprNotificationMessage : Repr NotificationMessage

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instToJsonNotificationMessage : Lean.ToJson NotificationMessage

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instFromJsonNotificationMessage : Lean.FromJson NotificationMessage

Equations

• One or more equations did not get rendered due to their size.

structure Lapis.Protocol.JsonRpc.ResponseMessage : Type

A JSON-RPC 2.0 successful response

• id : RequestId
• result : Lean.Json

instance Lapis.Protocol.JsonRpc.instInhabitedResponseMessage : Inhabited ResponseMessage

Equations

• Lapis.Protocol.JsonRpc.instInhabitedResponseMessage = { default := Lapis.Protocol.JsonRpc.instInhabitedResponseMessage.default }

def Lapis.Protocol.JsonRpc.instInhabitedResponseMessage.default : ResponseMessage

Equations

• Lapis.Protocol.JsonRpc.instInhabitedResponseMessage.default = { id := default, result := default }

instance Lapis.Protocol.JsonRpc.instReprResponseMessage : Repr ResponseMessage

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instToJsonResponseMessage : Lean.ToJson ResponseMessage

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instFromJsonResponseMessage : Lean.FromJson ResponseMessage

Equations

• One or more equations did not get rendered due to their size.

structure Lapis.Protocol.JsonRpc.ErrorResponseMessage : Type

A JSON-RPC 2.0 error response

• id : Option RequestId
• error : ResponseError

def Lapis.Protocol.JsonRpc.instInhabitedErrorResponseMessage.default : ErrorResponseMessage

Equations

• Lapis.Protocol.JsonRpc.instInhabitedErrorResponseMessage.default = { id := default, error := default }

instance Lapis.Protocol.JsonRpc.instInhabitedErrorResponseMessage : Inhabited ErrorResponseMessage

Equations

• Lapis.Protocol.JsonRpc.instInhabitedErrorResponseMessage = { default := Lapis.Protocol.JsonRpc.instInhabitedErrorResponseMessage.default }

instance Lapis.Protocol.JsonRpc.instReprErrorResponseMessage : Repr ErrorResponseMessage

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instToJsonErrorResponseMessage : Lean.ToJson ErrorResponseMessage

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instFromJsonErrorResponseMessage : Lean.FromJson ErrorResponseMessage

Equations

• One or more equations did not get rendered due to their size.

inductive Lapis.Protocol.JsonRpc.Message : Type

• request (msg : RequestMessage) : Message
• notification (msg : NotificationMessage) : Message
• response (msg : ResponseMessage) : Message
• errorResponse (msg : ErrorResponseMessage) : Message

instance Lapis.Protocol.JsonRpc.instInhabitedMessage : Inhabited Message

Equations

• Lapis.Protocol.JsonRpc.instInhabitedMessage = { default := Lapis.Protocol.JsonRpc.instInhabitedMessage.default }

def Lapis.Protocol.JsonRpc.instInhabitedMessage.default : Message

Equations

• Lapis.Protocol.JsonRpc.instInhabitedMessage.default = Lapis.Protocol.JsonRpc.Message.request default

def Lapis.Protocol.JsonRpc.instReprMessage.repr : Message → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instReprMessage : Repr Message

Equations

• Lapis.Protocol.JsonRpc.instReprMessage = { reprPrec := Lapis.Protocol.JsonRpc.instReprMessage.repr }

def Lapis.Protocol.JsonRpc.Message.fromJson? (json : Lean.Json) : Except String Message

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Protocol.JsonRpc.instFromJsonMessage : Lean.FromJson Message

Equations

• Lapis.Protocol.JsonRpc.instFromJsonMessage = { fromJson? := Lapis.Protocol.JsonRpc.Message.fromJson? }

def Lapis.Protocol.JsonRpc.Message.toJson : Message → Lean.Json

Equations

• (Lapis.Protocol.JsonRpc.Message.request a).toJson = Lean.toJson a
• (Lapis.Protocol.JsonRpc.Message.notification a).toJson = Lean.toJson a
• (Lapis.Protocol.JsonRpc.Message.response a).toJson = Lean.toJson a
• (Lapis.Protocol.JsonRpc.Message.errorResponse a).toJson = Lean.toJson a

instance Lapis.Protocol.JsonRpc.instToJsonMessage : Lean.ToJson Message

Equations

• Lapis.Protocol.JsonRpc.instToJsonMessage = { toJson := Lapis.Protocol.JsonRpc.Message.toJson }

def Lapis.Protocol.JsonRpc.mkResponse (id : RequestId) (result : Lean.Json) : Message

Equations

• Lapis.Protocol.JsonRpc.mkResponse id result = Lapis.Protocol.JsonRpc.Message.response { id := id, result := result }

def Lapis.Protocol.JsonRpc.mkErrorResponse (id : Option RequestId) (code : Int) (message : String) (data : Option Lean.Json := none) : Message

Equations

• Lapis.Protocol.JsonRpc.mkErrorResponse id code message data = Lapis.Protocol.JsonRpc.Message.errorResponse { id := id, error := { code := code, message := message, data := data } }

def Lapis.Protocol.JsonRpc.mkParseError (message : String) : Message

Equations

• Lapis.Protocol.JsonRpc.mkParseError message = Lapis.Protocol.JsonRpc.mkErrorResponse none Lapis.Protocol.JsonRpc.parseError message

def Lapis.Protocol.JsonRpc.mkInvalidRequest (id : Option RequestId) (message : String) : Message

Equations

• Lapis.Protocol.JsonRpc.mkInvalidRequest id message = Lapis.Protocol.JsonRpc.mkErrorResponse id Lapis.Protocol.JsonRpc.invalidRequest message

def Lapis.Protocol.JsonRpc.mkMethodNotFound (id : RequestId) (method : String) : Message

Equations

• Lapis.Protocol.JsonRpc.mkMethodNotFound id method = Lapis.Protocol.JsonRpc.mkErrorResponse (some id) Lapis.Protocol.JsonRpc.methodNotFound (toString "Method not found: " ++ toString method)

def Lapis.Protocol.JsonRpc.mkInvalidParams (id : RequestId) (message : String) : Message

Equations

• Lapis.Protocol.JsonRpc.mkInvalidParams id message = Lapis.Protocol.JsonRpc.mkErrorResponse (some id) Lapis.Protocol.JsonRpc.invalidParams message

def Lapis.Protocol.JsonRpc.mkInternalError (id : Option RequestId) (message : String) : Message

Equations

• Lapis.Protocol.JsonRpc.mkInternalError id message = Lapis.Protocol.JsonRpc.mkErrorResponse id Lapis.Protocol.JsonRpc.internalError message