instance Lean.Server.instInhabitedRpcProcedure : Inhabited Lean.Server.RpcProcedure✝

opaque Lean.Server.builtinRpcProcedures : IO.Ref (PHashMap Name Lean.Server.RpcProcedure✝)

opaque Lean.Server.userRpcProcedures : MapDeclarationExtension Name

@[implemented_by _private.Lean.Server.Rpc.RequestHandling.0.Lean.Server.evalRpcProcedureUnsafe]

opaque Lean.Server.evalRpcProcedure (env : Environment) (opts : Options) (procName : Name) : Except String Lean.Server.RpcProcedure✝

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)) : Lean.Server.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