def DocGen4.Process.TacticInfo.docStringToHtml (tac : TacticInfo MarkdownDocstring) : Output.HtmlM (TacticInfo Html)

Render the HTML for a single tactic.

Equations

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

def DocGen4.Process.TacticInfo.toHtml (tac : TacticInfo Html) : Output.BaseHtmlM Html

Render the HTML for a single tactic.

Equations

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

def DocGen4.Process.TacticInfo.navLink {α : Type} (tac : TacticInfo α) : Html

Equations

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

def DocGen4.Output.tactics (tacticInfo : Array (Process.TacticInfo Html)) : BaseHtmlM Html

Render the HTML for the tactics listing page.

Equations

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