Documentation

LeanRedis.Pipeline.Hash

source
def LeanRedis.Pipeline.hGet {α : List Type} (pipeline : Pipeline α) (key field : String) :
Pipeline (α ++ [Option String])
Equations
Instances For
    source
    def LeanRedis.Pipeline.hSet {α : List Type} (pipeline : Pipeline α) (key : String) (entries : Array (String × String)) :
    Pipeline (α ++ [Int])
    Equations
    Instances For
      source
      def LeanRedis.Pipeline.hMGet {α : List Type} (pipeline : Pipeline α) (key : String) (fields : Array String) :
      Pipeline (α ++ [Array (Option String)])
      Equations
      Instances For
        source
        def LeanRedis.Pipeline.hMSet {α : List Type} (pipeline : Pipeline α) (key : String) (entries : Array (String × String)) :
        Pipeline (α ++ [Unit])
        Equations
        Instances For
          source
          def LeanRedis.Pipeline.hGetAll {α : List Type} (pipeline : Pipeline α) (key : String) :
          Pipeline (α ++ [Array (String × String)])
          Equations
          Instances For
            source
            def LeanRedis.Pipeline.hDel {α : List Type} (pipeline : Pipeline α) (key : String) (fields : Array String) :
            Pipeline (α ++ [Int])
            Equations
            Instances For
              source
              def LeanRedis.Pipeline.hExists {α : List Type} (pipeline : Pipeline α) (key field : String) :
              Pipeline (α ++ [Bool])
              Equations
              Instances For
                source
                def LeanRedis.Pipeline.hLen {α : List Type} (pipeline : Pipeline α) (key : String) :
                Pipeline (α ++ [Int])
                Equations
                Instances For
                  source
                  def LeanRedis.Pipeline.hKeys {α : List Type} (pipeline : Pipeline α) (key : String) :
                  Pipeline (α ++ [Array String])
                  Equations
                  Instances For
                    source
                    def LeanRedis.Pipeline.hVals {α : List Type} (pipeline : Pipeline α) (key : String) :
                    Pipeline (α ++ [Array String])
                    Equations
                    Instances For
                      source
                      def LeanRedis.Pipeline.hStrLen {α : List Type} (pipeline : Pipeline α) (key field : String) :
                      Pipeline (α ++ [Int])
                      Equations
                      Instances For
                        source
                        def LeanRedis.Pipeline.hIncrBy {α : List Type} (pipeline : Pipeline α) (key field : String) (amount : Int) :
                        Pipeline (α ++ [Int])
                        Equations
                        Instances For
                          source
                          def LeanRedis.Pipeline.hIncrByFloat {α : List Type} (pipeline : Pipeline α) (key field amount : String) :
                          Pipeline (α ++ [String])
                          Equations
                          Instances For
                            source
                            def LeanRedis.Pipeline.hSetNx {α : List Type} (pipeline : Pipeline α) (key field value : String) :
                            Pipeline (α ++ [Bool])
                            Equations
                            Instances For
                              source
                              def LeanRedis.Pipeline.hRandField {α : List Type} (pipeline : Pipeline α) (key : String) :
                              Pipeline (α ++ [Option String])
                              Equations
                              Instances For
                                source
                                def LeanRedis.Pipeline.hRandFields {α : List Type} (pipeline : Pipeline α) (key : String) (count : Int) :
                                Pipeline (α ++ [Array String])
                                Equations
                                Instances For
                                  source
                                  def LeanRedis.Pipeline.hRandFieldsWithValues {α : List Type} (pipeline : Pipeline α) (key : String) (count : Int) :
                                  Pipeline (α ++ [Array (String × String)])
                                  Equations
                                  Instances For
                                    source
                                    def LeanRedis.Pipeline.hScan {α : List Type} (pipeline : Pipeline α) (key : String) (cursor : UInt64) (options : HScanOptions := { }) :
                                    Pipeline (α ++ [HashScanResult])
                                    Equations
                                    Instances For