← Mathematical handbook

inductive Lean.Linter.CodeQuality.Source : Type

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

@[instance_reducible]

instance Lean.Linter.CodeQuality.instToJsonSource : ToJson Source

Equations

• Lean.Linter.CodeQuality.instToJsonSource = { toJson := Lean.Linter.CodeQuality.instToJsonSource.toJson }

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Linter.CodeQuality.instToJsonSource.toJson (Lean.Linter.CodeQuality.Source.module a) = Lean.Json.mkObj [("module", Lean.Json.mkObj [("name", Lean.toJson a)])]

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

Equations

• Lean.Linter.CodeQuality.instToJsonValue = { toJson := Lean.Linter.CodeQuality.instToJsonValue.toJson }

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

Equations

• Lean.Linter.CodeQuality.instToJsonValue.toJson (Lean.Linter.CodeQuality.Value.scalar a) = Lean.Json.mkObj [("scalar", Lean.Json.mkObj [("value", Lean.toJson a)])]
• Lean.Linter.CodeQuality.instToJsonValue.toJson (Lean.Linter.CodeQuality.Value.dict a) = Lean.Json.mkObj [("dict", Lean.Json.mkObj [("dictionary", Lean.toJson a)])]

structure Lean.Linter.CodeQuality.Entry : Type

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

@[instance_reducible]

instance Lean.Linter.CodeQuality.instToJsonEntry : ToJson Entry

Equations

• Lean.Linter.CodeQuality.instToJsonEntry = { toJson := Lean.Linter.CodeQuality.instToJsonEntry.toJson }

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

Equations

• Lean.Linter.CodeQuality.instToJsonEntry.toJson x✝ = Lean.Json.mkObj [[("name", Lean.toJson x✝.name)], [("source", Lean.toJson x✝.source)], [("value", Lean.toJson x✝.value)]].flatten