def DocGen4.Output.structureInfoHeader (s : Process.StructureInfo) : HtmlM (Array Html)

Render the structures this structure extends from as HTML so it can be added to the top level.

Equations

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

def DocGen4.Output.docInfoHeader (doc : Process.DocInfo) : HtmlM Html

Render the general header of a declaration containing its declaration type and name.

Equations

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

def DocGen4.Output.docInfoToHtml (module : Lean.Name) (doc : Process.DocInfo) : HtmlM Html

The main entry point for rendering a single declaration inside a given module.

Equations

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

def DocGen4.Output.modDocToHtml (mdoc : Lean.ModuleDoc) : HtmlM Html

Rendering a module doc string, that is the ones with an ! after the opener as HTML.

Equations

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

def DocGen4.Output.moduleMemberToHtml (module : Lean.Name) (member : Process.ModuleMember) : HtmlM Html

Render a module member, that is either a module doc string or a declaration as HTML.

Equations

• DocGen4.Output.moduleMemberToHtml module (DocGen4.Process.ModuleMember.docInfo d) = DocGen4.Output.docInfoToHtml module d
• DocGen4.Output.moduleMemberToHtml module (DocGen4.Process.ModuleMember.modDoc d) = DocGen4.Output.modDocToHtml d

def DocGen4.Output.declarationToNavLink (module : Lean.Name) : Html

Equations

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

def DocGen4.Output.getImports (module : Lean.Name) : HtmlM (Array Lean.Name)

Returns the list of all imports this module does.

Equations

• DocGen4.Output.getImports module = do let res ← DocGen4.Output.getResult pure res.moduleInfo[module]!.imports

def DocGen4.Output.importsHtml (moduleName : Lean.Name) : HtmlM (Array Html)

Sort the list of all modules this one is importing, linkify it and return the HTML.

Equations

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

def DocGen4.Output.internalNav (members : Array Lean.Name) (moduleName : Lean.Name) : HtmlM Html

Render the internal nav bar (the thing on the right on all module pages).

Equations

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

def DocGen4.Output.moduleToHtml (module : Process.Module) : HtmlM Html

The main entry point to rendering the HTML for an entire module.

Equations

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