Documentation

LeanRedis.Pipeline.String

source
def LeanRedis.Pipeline.get {α : List Type} (pipeline : Pipeline α) (key : String) :
Pipeline (α ++ [Option String])
Equations
Instances For
    source
    def LeanRedis.Pipeline.set {α : List Type} (pipeline : Pipeline α) (key value : String) (options : SetOptions := { }) :
    Pipeline (α ++ [Bool])
    Equations
    Instances For
      source
      def LeanRedis.Pipeline.mGet {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
      Pipeline (α ++ [Array (Option String)])
      Equations
      Instances For
        source
        def LeanRedis.Pipeline.mSet {α : List Type} (pipeline : Pipeline α) (entries : Array (String × String)) :
        Pipeline (α ++ [Unit])
        Equations
        Instances For
          source
          def LeanRedis.Pipeline.mSetNx {α : List Type} (pipeline : Pipeline α) (entries : Array (String × String)) :
          Pipeline (α ++ [Bool])
          Equations
          Instances For
            source
            def LeanRedis.Pipeline.getDel {α : List Type} (pipeline : Pipeline α) (key : String) :
            Pipeline (α ++ [Option String])
            Equations
            Instances For
              source
              def LeanRedis.Pipeline.getEx {α : List Type} (pipeline : Pipeline α) (key : String) (mode? : Option GetExMode := none) :
              Pipeline (α ++ [Option String])
              Equations
              Instances For
                source
                def LeanRedis.Pipeline.getRange {α : List Type} (pipeline : Pipeline α) (key : String) (start stop : Int) :
                Pipeline (α ++ [String])
                Equations
                Instances For
                  source
                  def LeanRedis.Pipeline.getSet {α : List Type} (pipeline : Pipeline α) (key value : String) :
                  Pipeline (α ++ [Option String])
                  Equations
                  Instances For
                    source
                    def LeanRedis.Pipeline.setRange {α : List Type} (pipeline : Pipeline α) (key : String) (offset : UInt64) (value : String) :
                    Pipeline (α ++ [Int])
                    Equations
                    Instances For
                      source
                      def LeanRedis.Pipeline.strLen {α : List Type} (pipeline : Pipeline α) (key : String) :
                      Pipeline (α ++ [Int])
                      Equations
                      Instances For
                        source
                        def LeanRedis.Pipeline.append {α : List Type} (pipeline : Pipeline α) (key value : String) :
                        Pipeline (α ++ [Int])
                        Equations
                        Instances For
                          source
                          def LeanRedis.Pipeline.incr {α : List Type} (pipeline : Pipeline α) (key : String) :
                          Pipeline (α ++ [Int])
                          Equations
                          Instances For
                            source
                            def LeanRedis.Pipeline.incrBy {α : List Type} (pipeline : Pipeline α) (key : String) (amount : Int) :
                            Pipeline (α ++ [Int])
                            Equations
                            Instances For
                              source
                              def LeanRedis.Pipeline.incrByFloat {α : List Type} (pipeline : Pipeline α) (key amount : String) :
                              Pipeline (α ++ [String])
                              Equations
                              Instances For
                                source
                                def LeanRedis.Pipeline.decr {α : List Type} (pipeline : Pipeline α) (key : String) :
                                Pipeline (α ++ [Int])
                                Equations
                                Instances For
                                  source
                                  def LeanRedis.Pipeline.decrBy {α : List Type} (pipeline : Pipeline α) (key : String) (amount : Int) :
                                  Pipeline (α ++ [Int])
                                  Equations
                                  Instances For
                                    source
                                    def LeanRedis.Pipeline.setNx {α : List Type} (pipeline : Pipeline α) (key value : String) :
                                    Pipeline (α ++ [Bool])
                                    Equations
                                    Instances For
                                      source
                                      def LeanRedis.Pipeline.setEx {α : List Type} (pipeline : Pipeline α) (key : String) (seconds : UInt64) (value : String) :
                                      Pipeline (α ++ [Unit])
                                      Equations
                                      Instances For
                                        source
                                        def LeanRedis.Pipeline.pSetEx {α : List Type} (pipeline : Pipeline α) (key : String) (milliseconds : UInt64) (value : String) :
                                        Pipeline (α ++ [Unit])
                                        Equations
                                        Instances For