structure Lean.Server.RpcProcedure : Type

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

@[instance_reducible]

instance Lean.Server.instInhabitedRpcProcedure : Inhabited RpcProcedure

Equations

• Lean.Server.instInhabitedRpcProcedure = { default := Lean.Server.instInhabitedRpcProcedure.default }

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.

Equations

• Lean.Server.existsBuiltinRpcProcedure method = do let __do_lift ← ST.Ref.get Lean.Server.builtinRpcProcedures✝ pure (Lean.PersistentHashMap.contains __do_lift method)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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