Documentation

Lean.Server.Rpc.RequestHandling

source
instance Lean.Server.instInhabitedRpcProcedure :
Inhabited Lean.Server.RpcProcedure✝
source
opaque Lean.Server.builtinRpcProcedures :
IO.Ref (Lean.PHashMap Lean.Name Lean.Server.RpcProcedure✝)
source
opaque Lean.Server.userRpcProcedures :
Lean.MapDeclarationExtension Lean.Name
source
@[implemented_by _private.Lean.Server.Rpc.RequestHandling.0.Lean.Server.evalRpcProcedureUnsafe]
opaque Lean.Server.evalRpcProcedure (env : Lean.Environment) (opts : Lean.Options) (procName : Lean.Name) :
Except String Lean.Server.RpcProcedure✝
source
def Lean.Server.handleRpcCall (p : Lean.Lsp.RpcCallParams) :
Lean.Server.RequestM (Lean.Server.RequestTask Lean.Json)
Instances For
    source
    def Lean.Server.wrapRpcProcedure (method : Lean.Name) (paramType respType : Type) [Lean.Server.RpcEncodable paramType] [Lean.Server.RpcEncodable respType] (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.
    Instances For
      source
      def Lean.Server.registerBuiltinRpcProcedure (method : Lean.Name) (paramType respType : Type) [Lean.Server.RpcEncodable paramType] [Lean.Server.RpcEncodable respType] (handler : paramType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) :
      IO Unit
      Instances For
        source
        def Lean.Server.registerRpcProcedure (method : Lean.Name) :
        Lean.CoreM Unit
        Instances For