inductive LeanRedis.Protocol.Version : Type

• resp2 : Version
• resp3 : Version

@[implicit_reducible]

instance LeanRedis.Protocol.instBEqVersion : BEq Version

Equations

• LeanRedis.Protocol.instBEqVersion = { beq := LeanRedis.Protocol.instBEqVersion.beq }

def LeanRedis.Protocol.instBEqVersion.beq : Version → Version → Bool

Equations

• LeanRedis.Protocol.instBEqVersion.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def LeanRedis.Protocol.instInhabitedVersion.default : Version

Equations

• LeanRedis.Protocol.instInhabitedVersion.default = LeanRedis.Protocol.Version.resp2

@[implicit_reducible]

instance LeanRedis.Protocol.instInhabitedVersion : Inhabited Version

Equations

• LeanRedis.Protocol.instInhabitedVersion = { default := LeanRedis.Protocol.instInhabitedVersion.default }

@[implicit_reducible]

instance LeanRedis.Protocol.instReprVersion : Repr Version

Equations

• LeanRedis.Protocol.instReprVersion = { reprPrec := LeanRedis.Protocol.instReprVersion.repr }

def LeanRedis.Protocol.instReprVersion.repr : Version → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.