Documentation

LeanRedis.Pipeline.Set

source
def LeanRedis.Pipeline.sAdd {α : List Type} (pipeline : Pipeline α) (key : String) (members : Array String) :
Pipeline (α ++ [Int])
Equations
Instances For
    source
    def LeanRedis.Pipeline.sRem {α : List Type} (pipeline : Pipeline α) (key : String) (members : Array String) :
    Pipeline (α ++ [Int])
    Equations
    Instances For
      source
      def LeanRedis.Pipeline.sCard {α : List Type} (pipeline : Pipeline α) (key : String) :
      Pipeline (α ++ [Int])
      Equations
      Instances For
        source
        def LeanRedis.Pipeline.sIsMember {α : List Type} (pipeline : Pipeline α) (key member : String) :
        Pipeline (α ++ [Bool])
        Equations
        Instances For
          source
          def LeanRedis.Pipeline.sMIsMember {α : List Type} (pipeline : Pipeline α) (key : String) (members : Array String) :
          Pipeline (α ++ [Array Bool])
          Equations
          Instances For
            source
            def LeanRedis.Pipeline.sMembers {α : List Type} (pipeline : Pipeline α) (key : String) :
            Pipeline (α ++ [Array String])
            Equations
            Instances For
              source
              def LeanRedis.Pipeline.sPop {α : List Type} (pipeline : Pipeline α) (key : String) :
              Pipeline (α ++ [Option String])
              Equations
              Instances For
                source
                def LeanRedis.Pipeline.sPopMany {α : List Type} (pipeline : Pipeline α) (key : String) (count : UInt64) :
                Pipeline (α ++ [Array String])
                Equations
                Instances For
                  source
                  def LeanRedis.Pipeline.sRandMember {α : List Type} (pipeline : Pipeline α) (key : String) :
                  Pipeline (α ++ [Option String])
                  Equations
                  Instances For
                    source
                    def LeanRedis.Pipeline.sRandMembers {α : List Type} (pipeline : Pipeline α) (key : String) (count : Int) :
                    Pipeline (α ++ [Array String])
                    Equations
                    Instances For
                      source
                      def LeanRedis.Pipeline.sMove {α : List Type} (pipeline : Pipeline α) (source destination member : String) :
                      Pipeline (α ++ [Bool])
                      Equations
                      Instances For
                        source
                        def LeanRedis.Pipeline.sDiff {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
                        Pipeline (α ++ [Array String])
                        Equations
                        Instances For
                          source
                          def LeanRedis.Pipeline.sDiffStore {α : List Type} (pipeline : Pipeline α) (destination : String) (keys : Array String) :
                          Pipeline (α ++ [Int])
                          Equations
                          Instances For
                            source
                            def LeanRedis.Pipeline.sInter {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
                            Pipeline (α ++ [Array String])
                            Equations
                            Instances For
                              source
                              def LeanRedis.Pipeline.sInterCard {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
                              Pipeline (α ++ [Int])
                              Equations
                              Instances For
                                source
                                def LeanRedis.Pipeline.sInterStore {α : List Type} (pipeline : Pipeline α) (destination : String) (keys : Array String) :
                                Pipeline (α ++ [Int])
                                Equations
                                Instances For
                                  source
                                  def LeanRedis.Pipeline.sUnion {α : List Type} (pipeline : Pipeline α) (keys : Array String) :
                                  Pipeline (α ++ [Array String])
                                  Equations
                                  Instances For
                                    source
                                    def LeanRedis.Pipeline.sUnionStore {α : List Type} (pipeline : Pipeline α) (destination : String) (keys : Array String) :
                                    Pipeline (α ++ [Int])
                                    Equations
                                    Instances For
                                      source
                                      def LeanRedis.Pipeline.sScan {α : List Type} (pipeline : Pipeline α) (key : String) (cursor : UInt64) (options : SScanOptions := { }) :
                                      Pipeline (α ++ [SetScanResult])
                                      Equations
                                      Instances For