Documentation

Lean.Server.Rpc.RequestHandling

@[implemented_by _private.Lean.Server.Rpc.RequestHandling.0.Lean.Server.evalRpcProcedureUnsafe]
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Lean.Server.wrapRpcProcedure (method : Lake.Name) (paramType : Type) (respType : Type) [Lean.Server.RpcEncodable paramType] [Lean.Server.RpcEncodable respType] (handler : paramTypeLean.Server.RequestM (Lean.Server.RequestTask respType)) :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Lean.Server.registerBuiltinRpcProcedure (method : Lake.Name) (paramType : Type) (respType : Type) [Lean.Server.RpcEncodable paramType] [Lean.Server.RpcEncodable respType] (handler : paramTypeLean.Server.RequestM (Lean.Server.RequestTask respType)) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For