inductive LeanRedis.Protocol.Resp.Value : Type

• simpleString (value : String) : Value
• blobString (value : ByteArray) : Value
• simpleError (message : String) : Value
• number (value : Int) : Value
• null : Value
• array (items : Array Value) : Value
• map (entries : Array (Value × Value)) : Value
• set (items : Array Value) : Value
• bool (value : Bool) : Value
• double (value : String) : Value
• bigNumber (value : String) : Value
• verbatimString (format value : String) : Value
• push (items : Array Value) : Value

@[implicit_reducible]

instance LeanRedis.Protocol.Resp.instBEqValue : BEq Value

Equations

• LeanRedis.Protocol.Resp.instBEqValue = { beq := LeanRedis.Protocol.Resp.instBEqValue.beq }

partial def LeanRedis.Protocol.Resp.instBEqValue.beq : Value → Value → Bool

def LeanRedis.Protocol.Resp.instInhabitedValue.default : Value

Equations

• LeanRedis.Protocol.Resp.instInhabitedValue.default = LeanRedis.Protocol.Resp.Value.simpleString default

@[implicit_reducible]

instance LeanRedis.Protocol.Resp.instInhabitedValue : Inhabited Value

Equations

• LeanRedis.Protocol.Resp.instInhabitedValue = { default := LeanRedis.Protocol.Resp.instInhabitedValue.default }

@[implicit_reducible]

instance LeanRedis.Protocol.Resp.instReprValue : Repr Value

Equations

• LeanRedis.Protocol.Resp.instReprValue = { reprPrec := fun (value : LeanRedis.Protocol.Resp.Value) (x : Nat) => Std.Format.text (LeanRedis.Protocol.Resp.render✝ value) }