def DocGen4.Output.moduleListFile (file : Lean.Name) : BaseHtmlM Html

Equations

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

partial def DocGen4.Output.moduleListDir (h : Hierarchy) : BaseHtmlM Html

Build the HTML tree representing the module hierarchy.

def DocGen4.Output.moduleList : BaseHtmlM Html

Return a list of top level modules, linkified and rendered as HTML

Equations

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

def DocGen4.Output.navbar : BaseHtmlM Html

The main entry point to rendering the navbar on the left hand side.

Equations

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