structure Lean.Server.RpcProcedure : Type

• wrapper (sessionId : UInt64) : Json → RequestM (RequestTask Json)

@[instance_reducible]

instance Lean.Server.instInhabitedRpcProcedure : Inhabited RpcProcedure

opaque Lean.Server.userRpcProcedures : MapDeclarationExtension Name

def Lean.Server.existsBuiltinRpcProcedure (method : Name) : IO Bool

Checks whether a builtin RPC procedure exists with the given name.

def Lean.Server.handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json)

def Lean.Server.wrapRpcProcedure (method : Name) (paramType respType : Type) [RpcEncodable paramType] [RpcEncodable respType] (handler : paramType → RequestM (RequestTask respType)) : RpcProcedure

def Lean.Server.registerBuiltinRpcProcedure (method : Name) (paramType respType : Type) [RpcEncodable paramType] [RpcEncodable respType] (handler : paramType → RequestM (RequestTask respType)) : IO Unit

def Lean.Server.registerRpcProcedure (method : Name) : CoreM Unit