@[reducible, inline]
Redacted constant string
Equations
- LeanRedis.REDACTED = "<REDACTED>"
Instances For
A type for representing values that should be redacted in logs and error messages.
Instances For
@[implicit_reducible]
Equations
Equations
- LeanRedis.instBEqRedacted.beq { value := a } { value := b } = (a == b)
- LeanRedis.instBEqRedacted.beq x✝¹ x✝ = false
Instances For
@[implicit_reducible]
Equations
Equations
- LeanRedis.instInhabitedRedacted.default = { value := default }
Instances For
@[implicit_reducible]
Equations
- LeanRedis.Redacted.instRepr = { reprPrec := fun (x : LeanRedis.Redacted) (x_1 : Nat) => Std.Format.text LeanRedis.REDACTED }
@[implicit_reducible]
Equations
- LeanRedis.Redacted.instToString = { toString := fun (x : LeanRedis.Redacted) => LeanRedis.REDACTED }