source
structure Lean.Server.RpcProcedure :
Type

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

Instances For

source
def Lean.Server.instInhabitedRpcProcedure.default :
RpcProcedure
Equations

- Lean.Server.instInhabitedRpcProcedure.default = { wrapper := default }

Instances For

source
instance Lean.Server.instInhabitedRpcProcedure :
Inhabited RpcProcedure
Equations

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

source
opaque Lean.Server.userRpcProcedures :
MapDeclarationExtension Name
source
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)

Instances For

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

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

Instances For

source
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.

Instances For

source
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.

Instances For

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

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

Instances For