Documentation

Lean.Server.Rpc.RequestHandling

source
instance Lean.Server.instInhabitedRpcProcedure:
Inhabited Lean.Server.RpcProcedure
Equations
source
opaque Lean.Server.builtinRpcProcedures:
IO.Ref (Std.PHashMap Lean.Name Lean.Server.RpcProcedure)
source
opaque Lean.Server.userRpcProcedures:
Lean.MapDeclarationExtension Lean.Name
source
def Lean.Server.wrapRpcProcedure (method : Lean.Name) (paramType : Type) (respType : Type) {paramLspType : Type} [inst : Lean.Server.RpcEncoding paramType paramLspType] [inst : Lean.FromJson paramLspType] {respLspType : Type} [inst : Lean.Server.RpcEncoding respType respLspType] [inst : Lean.ToJson respLspType] (handler : paramType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) :
Lean.Server.RpcProcedure
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.registerBuiltinRpcProcedure (method : Lean.Name) (paramType : Type) (respType : Type) {paramLspType : Type} [inst : Lean.Server.RpcEncoding paramType paramLspType] [inst : Lean.FromJson paramLspType] {respLspType : Type} [inst : Lean.Server.RpcEncoding respType respLspType] [inst : Lean.ToJson respLspType] (handler : paramType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) :
IO Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.registerRpcProcedure (method : Lean.Name) :
Lean.CoreM Unit
Equations
  • One or more equations did not get rendered due to their size.