Documentation

LeanRedis.Pipeline.Generic

source
def LeanRedis.Pipeline.copy {α : List Type} (pipeline : Pipeline α) (source destination : String) (options : CopyOptions := { }) :
Pipeline (α ++ [Bool])
Equations
Instances For
    source
    def LeanRedis.Pipeline.del {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
    Pipeline (α ++ [Int])
    Equations
    Instances For
      source
      def LeanRedis.Pipeline.dump {α : List Type} (pipeline : Pipeline α) (key : String) :
      Pipeline (α ++ [String])
      Equations
      Instances For
        source
        def LeanRedis.Pipeline.exists {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
        Pipeline (α ++ [Int])
        Equations
        Instances For
          source
          def LeanRedis.Pipeline.expire {α : List Type} (pipeline : Pipeline α) (key : String) (seconds : UInt64) (option : Option ExpireOption := none) :
          Pipeline (α ++ [Bool])
          Equations
          Instances For
            source
            def LeanRedis.Pipeline.expireAt {α : List Type} (pipeline : Pipeline α) (key : String) (timestamp : Std.Time.Timestamp) (option : Option ExpireOption := none) :
            Pipeline (α ++ [Bool])
            Equations
            Instances For
              source
              def LeanRedis.Pipeline.expireTime {α : List Type} (pipeline : Pipeline α) (key : String) :
              Pipeline (α ++ [Int])
              Equations
              Instances For
                source
                def LeanRedis.Pipeline.keys {α : List Type} (pipeline : Pipeline α) (pattern : String) :
                Pipeline (α ++ [Array String])
                Equations
                Instances For
                  source
                  def LeanRedis.Pipeline.move {α : List Type} (pipeline : Pipeline α) (key : String) (destinationDb : UInt32) :
                  Pipeline (α ++ [Bool])
                  Equations
                  Instances For
                    source
                    def LeanRedis.Pipeline.objectEncoding {α : List Type} (pipeline : Pipeline α) (key : String) :
                    Pipeline (α ++ [String])
                    Equations
                    Instances For
                      source
                      def LeanRedis.Pipeline.objectFreq {α : List Type} (pipeline : Pipeline α) (key : String) :
                      Pipeline (α ++ [Int])
                      Equations
                      Instances For
                        source
                        def LeanRedis.Pipeline.objectIdleTime {α : List Type} (pipeline : Pipeline α) (key : String) :
                        Pipeline (α ++ [Int])
                        Equations
                        Instances For
                          source
                          def LeanRedis.Pipeline.objectRefCount {α : List Type} (pipeline : Pipeline α) (key : String) :
                          Pipeline (α ++ [Int])
                          Equations
                          Instances For
                            source
                            def LeanRedis.Pipeline.persist {α : List Type} (pipeline : Pipeline α) (key : String) :
                            Pipeline (α ++ [Bool])
                            Equations
                            Instances For
                              source
                              def LeanRedis.Pipeline.pexpire {α : List Type} (pipeline : Pipeline α) (key : String) (milliseconds : UInt64) (option : Option ExpireOption := none) :
                              Pipeline (α ++ [Bool])
                              Equations
                              Instances For
                                source
                                def LeanRedis.Pipeline.pexpireAt {α : List Type} (pipeline : Pipeline α) (key : String) (timestamp : Std.Time.Timestamp) (option : Option ExpireOption := none) :
                                Pipeline (α ++ [Bool])
                                Equations
                                Instances For
                                  source
                                  def LeanRedis.Pipeline.pttl {α : List Type} (pipeline : Pipeline α) (key : String) :
                                  Pipeline (α ++ [Int])
                                  Equations
                                  Instances For
                                    source
                                    def LeanRedis.Pipeline.randomKey {α : List Type} (pipeline : Pipeline α) :
                                    Pipeline (α ++ [Option String])
                                    Equations
                                    Instances For
                                      source
                                      def LeanRedis.Pipeline.rename {α : List Type} (pipeline : Pipeline α) (key newKey : String) :
                                      Pipeline (α ++ [Unit])
                                      Equations
                                      Instances For
                                        source
                                        def LeanRedis.Pipeline.renameNx {α : List Type} (pipeline : Pipeline α) (key newKey : String) :
                                        Pipeline (α ++ [Bool])
                                        Equations
                                        Instances For
                                          source
                                          def LeanRedis.Pipeline.restore {α : List Type} (pipeline : Pipeline α) (key : String) (ttl : UInt64) (serializedValue : String) (options : RestoreOptions := { }) :
                                          Pipeline (α ++ [Unit])
                                          Equations
                                          Instances For
                                            source
                                            def LeanRedis.Pipeline.scan {α : List Type} (pipeline : Pipeline α) (cursor : UInt64) (options : ScanOptions := { }) :
                                            Pipeline (α ++ [ScanResult])
                                            Equations
                                            Instances For
                                              source
                                              def LeanRedis.Pipeline.sort {α : List Type} (pipeline : Pipeline α) (key : String) (options : SortOptions := { }) :
                                              Pipeline (α ++ [Array String])
                                              Equations
                                              Instances For
                                                source
                                                def LeanRedis.Pipeline.sortRo {α : List Type} (pipeline : Pipeline α) (key : String) (options : SortRoOptions := { }) :
                                                Pipeline (α ++ [Array String])
                                                Equations
                                                Instances For
                                                  source
                                                  def LeanRedis.Pipeline.touch {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
                                                  Pipeline (α ++ [Int])
                                                  Equations
                                                  Instances For
                                                    source
                                                    def LeanRedis.Pipeline.ttl {α : List Type} (pipeline : Pipeline α) (key : String) :
                                                    Pipeline (α ++ [Int])
                                                    Equations
                                                    Instances For
                                                      source
                                                      def LeanRedis.Pipeline.type {α : List Type} (pipeline : Pipeline α) (key : String) :
                                                      Pipeline (α ++ [String])
                                                      Equations
                                                      Instances For