Documentation

Lean.Server.Rpc.RequestHandling

def Lean.Server.registerRpcCallHandler (method : Lean.Name) (paramType : Type) (respType : Type) {paramLspType : outParam Type} [inst : Lean.Server.RpcEncoding paramType paramLspType] [inst : Lean.FromJson paramLspType] {respLspType : outParam Type} [inst : Lean.Server.RpcEncoding respType respLspType] [inst : Lean.ToJson respLspType] (handler : paramTypeLean.Server.RequestM (Lean.Server.RequestTask respType)) :
Equations