Documentation

Lapis.Server.Receiver

source
structure Lapis.Server.Receiver.PendingResponses :
Type

Tracks pending responses for server-initiated requests. Uses atomic IO.Ref operations - no mutex needed.

Instances For
    source
    def Lapis.Server.Receiver.PendingResponses.new :
    IO PendingResponses
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lapis.Server.Receiver.PendingResponses.register (pr : PendingResponses) (promise : IO.Promise Lean.Json) :
      IO Protocol.JsonRpc.RequestId
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lapis.Server.Receiver.PendingResponses.execute (pr : PendingResponses) (id : Protocol.JsonRpc.RequestId) (payload : Lean.Json) :
        IO Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lapis.Server.Receiver.PendingResponses.executeError (pr : PendingResponses) (id : Protocol.JsonRpc.RequestId) (error : String) :
          IO Unit
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For