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

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

opaque Lean.Server.userRpcProcedures : Lean.MapDeclarationExtension Lake.Name

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

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

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

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

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

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