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
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
JSON-RPC 2.0 error codes
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
A JSON-RPC 2.0 successful response
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
- request (msg : RequestMessage) : Message
- notification (msg : NotificationMessage) : Message
- response (msg : ResponseMessage) : Message
- errorResponse (msg : ErrorResponseMessage) : Message
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
Instances For
Equations
- Lapis.Protocol.JsonRpc.mkResponse id result = Lapis.Protocol.JsonRpc.Message.response { id := id, result := result }
Instances For
def
Lapis.Protocol.JsonRpc.mkErrorResponse
(id : Option RequestId)
(code : Int)
(message : String)
(data : Option Lean.Json := none)
:
Equations
- Lapis.Protocol.JsonRpc.mkErrorResponse id code message data = Lapis.Protocol.JsonRpc.Message.errorResponse { id := id, error := { code := code, message := message, data := data } }
Instances For
Equations
Instances For
Equations
Instances For
Equations
- Lapis.Protocol.JsonRpc.mkMethodNotFound id method = Lapis.Protocol.JsonRpc.mkErrorResponse (some id) Lapis.Protocol.JsonRpc.methodNotFound (toString "Method not found: " ++ toString method)