Documentation

LeanRedis.Pipeline.SortedSet

source
def LeanRedis.Pipeline.zAdd {α : List Type} (pipeline : Pipeline α) (key : String) (entries : Array SortedSetEntry) :
Pipeline (α ++ [Int])
Equations
Instances For
    source
    def LeanRedis.Pipeline.zRem {α : List Type} (pipeline : Pipeline α) (key : String) (members : Array String) :
    Pipeline (α ++ [Int])
    Equations
    Instances For
      source
      def LeanRedis.Pipeline.zCard {α : List Type} (pipeline : Pipeline α) (key : String) :
      Pipeline (α ++ [Int])
      Equations
      Instances For
        source
        def LeanRedis.Pipeline.zScore {α : List Type} (pipeline : Pipeline α) (key member : String) :
        Pipeline (α ++ [Option String])
        Equations
        Instances For
          source
          def LeanRedis.Pipeline.zMScore {α : List Type} (pipeline : Pipeline α) (key : String) (members : Array String) :
          Pipeline (α ++ [Array (Option String)])
          Equations
          Instances For
            source
            def LeanRedis.Pipeline.zRank {α : List Type} (pipeline : Pipeline α) (key member : String) :
            Pipeline (α ++ [Option Int])
            Equations
            Instances For
              source
              def LeanRedis.Pipeline.zRevRank {α : List Type} (pipeline : Pipeline α) (key member : String) :
              Pipeline (α ++ [Option Int])
              Equations
              Instances For
                source
                def LeanRedis.Pipeline.zRange {α : List Type} (pipeline : Pipeline α) (key : String) (start stop : Int) :
                Pipeline (α ++ [Array String])
                Equations
                Instances For
                  source
                  def LeanRedis.Pipeline.zRangeWithScores {α : List Type} (pipeline : Pipeline α) (key : String) (start stop : Int) :
                  Pipeline (α ++ [Array SortedSetEntry])
                  Equations
                  Instances For
                    source
                    def LeanRedis.Pipeline.zRevRange {α : List Type} (pipeline : Pipeline α) (key : String) (start stop : Int) :
                    Pipeline (α ++ [Array String])
                    Equations
                    Instances For
                      source
                      def LeanRedis.Pipeline.zRevRangeWithScores {α : List Type} (pipeline : Pipeline α) (key : String) (start stop : Int) :
                      Pipeline (α ++ [Array SortedSetEntry])
                      Equations
                      Instances For
                        source
                        def LeanRedis.Pipeline.zRangeByScore {α : List Type} (pipeline : Pipeline α) (key min max : String) :
                        Pipeline (α ++ [Array String])
                        Equations
                        Instances For
                          source
                          def LeanRedis.Pipeline.zRangeByScoreWithScores {α : List Type} (pipeline : Pipeline α) (key min max : String) :
                          Pipeline (α ++ [Array SortedSetEntry])
                          Equations
                          Instances For
                            source
                            def LeanRedis.Pipeline.zRevRangeByScore {α : List Type} (pipeline : Pipeline α) (key max min : String) :
                            Pipeline (α ++ [Array String])
                            Equations
                            Instances For
                              source
                              def LeanRedis.Pipeline.zRevRangeByScoreWithScores {α : List Type} (pipeline : Pipeline α) (key max min : String) :
                              Pipeline (α ++ [Array SortedSetEntry])
                              Equations
                              Instances For
                                source
                                def LeanRedis.Pipeline.zRangeByLex {α : List Type} (pipeline : Pipeline α) (key min max : String) :
                                Pipeline (α ++ [Array String])
                                Equations
                                Instances For
                                  source
                                  def LeanRedis.Pipeline.zRevRangeByLex {α : List Type} (pipeline : Pipeline α) (key max min : String) :
                                  Pipeline (α ++ [Array String])
                                  Equations
                                  Instances For
                                    source
                                    def LeanRedis.Pipeline.zCount {α : List Type} (pipeline : Pipeline α) (key min max : String) :
                                    Pipeline (α ++ [Int])
                                    Equations
                                    Instances For
                                      source
                                      def LeanRedis.Pipeline.zLexCount {α : List Type} (pipeline : Pipeline α) (key min max : String) :
                                      Pipeline (α ++ [Int])
                                      Equations
                                      Instances For
                                        source
                                        def LeanRedis.Pipeline.zRemRangeByRank {α : List Type} (pipeline : Pipeline α) (key : String) (start stop : Int) :
                                        Pipeline (α ++ [Int])
                                        Equations
                                        Instances For
                                          source
                                          def LeanRedis.Pipeline.zRemRangeByScore {α : List Type} (pipeline : Pipeline α) (key min max : String) :
                                          Pipeline (α ++ [Int])
                                          Equations
                                          Instances For
                                            source
                                            def LeanRedis.Pipeline.zRemRangeByLex {α : List Type} (pipeline : Pipeline α) (key min max : String) :
                                            Pipeline (α ++ [Int])
                                            Equations
                                            Instances For
                                              source
                                              def LeanRedis.Pipeline.zIncrBy {α : List Type} (pipeline : Pipeline α) (key increment member : String) :
                                              Pipeline (α ++ [String])
                                              Equations
                                              Instances For
                                                source
                                                def LeanRedis.Pipeline.zRandMember {α : List Type} (pipeline : Pipeline α) (key : String) :
                                                Pipeline (α ++ [Option String])
                                                Equations
                                                Instances For
                                                  source
                                                  def LeanRedis.Pipeline.zRandMembers {α : List Type} (pipeline : Pipeline α) (key : String) (count : Int) :
                                                  Pipeline (α ++ [Array String])
                                                  Equations
                                                  Instances For
                                                    source
                                                    def LeanRedis.Pipeline.zRandMembersWithScores {α : List Type} (pipeline : Pipeline α) (key : String) (count : Int) :
                                                    Pipeline (α ++ [Array SortedSetEntry])
                                                    Equations
                                                    Instances For
                                                      source
                                                      def LeanRedis.Pipeline.zDiff {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
                                                      Pipeline (α ++ [Array String])
                                                      Equations
                                                      Instances For
                                                        source
                                                        def LeanRedis.Pipeline.zDiffStore {α : List Type} (pipeline : Pipeline α) (destination : String) (keys : Array String) :
                                                        Pipeline (α ++ [Int])
                                                        Equations
                                                        Instances For
                                                          source
                                                          def LeanRedis.Pipeline.zInter {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
                                                          Pipeline (α ++ [Array String])
                                                          Equations
                                                          Instances For
                                                            source
                                                            def LeanRedis.Pipeline.zInterCard {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
                                                            Pipeline (α ++ [Int])
                                                            Equations
                                                            Instances For
                                                              source
                                                              def LeanRedis.Pipeline.zInterStore {α : List Type} (pipeline : Pipeline α) (destination : String) (keys : Array String) :
                                                              Pipeline (α ++ [Int])
                                                              Equations
                                                              Instances For
                                                                source
                                                                def LeanRedis.Pipeline.zUnion {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
                                                                Pipeline (α ++ [Array String])
                                                                Equations
                                                                Instances For
                                                                  source
                                                                  def LeanRedis.Pipeline.zUnionStore {α : List Type} (pipeline : Pipeline α) (destination : String) (keys : Array String) :
                                                                  Pipeline (α ++ [Int])
                                                                  Equations
                                                                  Instances For
                                                                    source
                                                                    def LeanRedis.Pipeline.zScan {α : List Type} (pipeline : Pipeline α) (key : String) (cursor : UInt64) (options : ZScanOptions := { }) :
                                                                    Pipeline (α ++ [SortedSetScanResult])
                                                                    Equations
                                                                    Instances For