structure DocGen4.Output.JsonDeclarationInfo : Type

• name : String
• kind : String
• doc : String
• docLink : String
• sourceLink : String
• line : Nat

def DocGen4.Output.instFromJsonJsonDeclarationInfo.fromJson : Lean.Json → Except String JsonDeclarationInfo

Equations

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

@[implicit_reducible]

instance DocGen4.Output.instFromJsonJsonDeclarationInfo : Lean.FromJson JsonDeclarationInfo

Equations

• DocGen4.Output.instFromJsonJsonDeclarationInfo = { fromJson? := DocGen4.Output.instFromJsonJsonDeclarationInfo.fromJson }

@[implicit_reducible]

instance DocGen4.Output.instToJsonJsonDeclarationInfo : Lean.ToJson JsonDeclarationInfo

Equations

• DocGen4.Output.instToJsonJsonDeclarationInfo = { toJson := DocGen4.Output.instToJsonJsonDeclarationInfo.toJson }

def DocGen4.Output.instToJsonJsonDeclarationInfo.toJson : JsonDeclarationInfo → Lean.Json

Equations

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

structure DocGen4.Output.JsonDeclaration : Type

• info : JsonDeclarationInfo
• header : String

@[implicit_reducible]

instance DocGen4.Output.instFromJsonJsonDeclaration : Lean.FromJson JsonDeclaration

Equations

• DocGen4.Output.instFromJsonJsonDeclaration = { fromJson? := DocGen4.Output.instFromJsonJsonDeclaration.fromJson }

def DocGen4.Output.instFromJsonJsonDeclaration.fromJson : Lean.Json → Except String JsonDeclaration

Equations

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

def DocGen4.Output.instToJsonJsonDeclaration.toJson : JsonDeclaration → Lean.Json

Equations

• DocGen4.Output.instToJsonJsonDeclaration.toJson x✝ = Lean.Json.mkObj [[("info", Lean.toJson x✝.info)], [("header", Lean.toJson x✝.header)]].flatten

@[implicit_reducible]

instance DocGen4.Output.instToJsonJsonDeclaration : Lean.ToJson JsonDeclaration

Equations

• DocGen4.Output.instToJsonJsonDeclaration = { toJson := DocGen4.Output.instToJsonJsonDeclaration.toJson }

structure DocGen4.Output.JsonInstance : Type

• name : String
• className : String
• typeNames : Array String

def DocGen4.Output.instFromJsonJsonInstance.fromJson : Lean.Json → Except String JsonInstance

Equations

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

@[implicit_reducible]

instance DocGen4.Output.instFromJsonJsonInstance : Lean.FromJson JsonInstance

Equations

• DocGen4.Output.instFromJsonJsonInstance = { fromJson? := DocGen4.Output.instFromJsonJsonInstance.fromJson }

def DocGen4.Output.instToJsonJsonInstance.toJson : JsonInstance → Lean.Json

Equations

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

@[implicit_reducible]

instance DocGen4.Output.instToJsonJsonInstance : Lean.ToJson JsonInstance

Equations

• DocGen4.Output.instToJsonJsonInstance = { toJson := DocGen4.Output.instToJsonJsonInstance.toJson }

structure DocGen4.Output.JsonModule : Type

• name : String
• declarations : List JsonDeclaration
• instances : Array JsonInstance
• imports : Array String

@[implicit_reducible]

instance DocGen4.Output.instFromJsonJsonModule : Lean.FromJson JsonModule

Equations

• DocGen4.Output.instFromJsonJsonModule = { fromJson? := DocGen4.Output.instFromJsonJsonModule.fromJson }

def DocGen4.Output.instFromJsonJsonModule.fromJson : Lean.Json → Except String JsonModule

Equations

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

@[implicit_reducible]

instance DocGen4.Output.instToJsonJsonModule : Lean.ToJson JsonModule

Equations

• DocGen4.Output.instToJsonJsonModule = { toJson := DocGen4.Output.instToJsonJsonModule.toJson }

def DocGen4.Output.instToJsonJsonModule.toJson : JsonModule → Lean.Json

Equations

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

structure DocGen4.Output.JsonHeaderIndex : Type

• declarations : List (String × JsonDeclaration)

structure DocGen4.Output.JsonIndexedDeclarationInfo : Type

• kind : String
• docLink : String

def DocGen4.Output.instFromJsonJsonIndexedDeclarationInfo.fromJson : Lean.Json → Except String JsonIndexedDeclarationInfo

Equations

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

@[implicit_reducible]

instance DocGen4.Output.instFromJsonJsonIndexedDeclarationInfo : Lean.FromJson JsonIndexedDeclarationInfo

Equations

• DocGen4.Output.instFromJsonJsonIndexedDeclarationInfo = { fromJson? := DocGen4.Output.instFromJsonJsonIndexedDeclarationInfo.fromJson }

def DocGen4.Output.instToJsonJsonIndexedDeclarationInfo.toJson : JsonIndexedDeclarationInfo → Lean.Json

Equations

• DocGen4.Output.instToJsonJsonIndexedDeclarationInfo.toJson x✝ = Lean.Json.mkObj [[("kind", Lean.toJson x✝.kind)], [("docLink", Lean.toJson x✝.docLink)]].flatten

@[implicit_reducible]

instance DocGen4.Output.instToJsonJsonIndexedDeclarationInfo : Lean.ToJson JsonIndexedDeclarationInfo

Equations

• DocGen4.Output.instToJsonJsonIndexedDeclarationInfo = { toJson := DocGen4.Output.instToJsonJsonIndexedDeclarationInfo.toJson }

structure DocGen4.Output.JsonIndexedModule : Type

• importedBy : Array String
• url : String

@[implicit_reducible]

instance DocGen4.Output.instFromJsonJsonIndexedModule : Lean.FromJson JsonIndexedModule

Equations

• DocGen4.Output.instFromJsonJsonIndexedModule = { fromJson? := DocGen4.Output.instFromJsonJsonIndexedModule.fromJson }

def DocGen4.Output.instFromJsonJsonIndexedModule.fromJson : Lean.Json → Except String JsonIndexedModule

Equations

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

def DocGen4.Output.instToJsonJsonIndexedModule.toJson : JsonIndexedModule → Lean.Json

Equations

• DocGen4.Output.instToJsonJsonIndexedModule.toJson x✝ = Lean.Json.mkObj [[("importedBy", Lean.toJson x✝.importedBy)], [("url", Lean.toJson x✝.url)]].flatten

@[implicit_reducible]

instance DocGen4.Output.instToJsonJsonIndexedModule : Lean.ToJson JsonIndexedModule

Equations

• DocGen4.Output.instToJsonJsonIndexedModule = { toJson := DocGen4.Output.instToJsonJsonIndexedModule.toJson }

structure DocGen4.Output.JsonIndex : Type

• declarations : List (String × JsonIndexedDeclarationInfo)
• instances : Std.HashMap String (Lean.RBTree String compare)
• modules : Std.HashMap String JsonIndexedModule
• instancesFor : Std.HashMap String (Lean.RBTree String compare)

@[implicit_reducible]

instance DocGen4.Output.instToJsonJsonHeaderIndex : Lean.ToJson JsonHeaderIndex

Equations

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

@[implicit_reducible]

instance DocGen4.Output.instToJsonJsonIndex : Lean.ToJson JsonIndex

Equations

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

def DocGen4.Output.JsonHeaderIndex.addModule (index : JsonHeaderIndex) (module : JsonModule) : JsonHeaderIndex

Equations

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

def DocGen4.Output.JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM JsonIndex

Equations

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

def DocGen4.Output.DocInfo.toJson (sourceLinker : Option Lean.DeclarationRange → String) (info : Process.DocInfo) : HtmlM JsonDeclaration

Equations

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

def DocGen4.Output.moduleToJsonModule (module : Process.Module) : HtmlM JsonModule

Equations

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

def DocGen4.Output.Process.Module.toJson (module : Process.Module) : HtmlM Lean.Json

Equations

• DocGen4.Output.Process.Module.toJson module = do let __do_lift ← DocGen4.Output.moduleToJsonModule module pure (Lean.toJson __do_lift)