@[reducible, inline]

abbrev LeanRedis.REDACTED : String

Redacted constant string

Equations

• LeanRedis.REDACTED = "<REDACTED>"

structure LeanRedis.Redacted : Type

A type for representing values that should be redacted in logs and error messages.

• value : String
• value : String

@[implicit_reducible]

instance LeanRedis.instBEqRedacted : BEq Redacted

Equations

• LeanRedis.instBEqRedacted = { beq := LeanRedis.instBEqRedacted.beq }

def LeanRedis.instBEqRedacted.beq : Redacted → Redacted → Bool

Equations

• LeanRedis.instBEqRedacted.beq { value := a } { value := b } = (a == b)
• LeanRedis.instBEqRedacted.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instInhabitedRedacted : Inhabited Redacted

Equations

• LeanRedis.instInhabitedRedacted = { default := LeanRedis.instInhabitedRedacted.default }

def LeanRedis.instInhabitedRedacted.default : Redacted

Equations

• LeanRedis.instInhabitedRedacted.default = { value := default }

@[implicit_reducible]

instance LeanRedis.Redacted.instRepr : Repr Redacted

Equations

• LeanRedis.Redacted.instRepr = { reprPrec := fun (x : LeanRedis.Redacted) (x_1 : Nat) => Std.Format.text LeanRedis.REDACTED }

@[implicit_reducible]

instance LeanRedis.Redacted.instToString : ToString Redacted

Equations

• LeanRedis.Redacted.instToString = { toString := fun (x : LeanRedis.Redacted) => LeanRedis.REDACTED }

@[implicit_reducible]

instance LeanRedis.Redacted.instCoeString : Coe String Redacted

Equations

• LeanRedis.Redacted.instCoeString = { coe := fun (str : String) => { value := str } }

def LeanRedis.Redacted.expose (redacted : Redacted) : String

Exposes the underlying value of a Redacted instance.

Equations

• redacted.expose = redacted.value