inductive Lean.Linter.CodeQuality.Source : Type

• module (name : Name) : Source
• declaration (module name : Name) : Source

@[instance_reducible]

instance Lean.Linter.CodeQuality.instToJsonSource : ToJson Source

def Lean.Linter.CodeQuality.instToJsonSource.toJson : Source → Json

inductive Lean.Linter.CodeQuality.Value : Type

• scalar (value : Float) : Value
• dict (dictionary : Std.TreeMap String Float compare) : Value

@[instance_reducible]

instance Lean.Linter.CodeQuality.instToJsonValue : ToJson Value

def Lean.Linter.CodeQuality.instToJsonValue.toJson : Value → Json

structure Lean.Linter.CodeQuality.Entry : Type

• name : String
• source : Source
• value : Value

@[instance_reducible]

instance Lean.Linter.CodeQuality.instToJsonEntry : ToJson Entry

def Lean.Linter.CodeQuality.instToJsonEntry.toJson : Entry → Json