This module contains helpers used for formatting hovers according to docstring conventions. Links to the reference manual are updated in the module Lean.DocString.Links, because that functionality is not specific to hovers.

source
def Lean.Server.FileWorker.Hover.rewriteExamples (docstring : String) :
String

Rewrites examples in docstring Markdown for output as hover Markdown.

In particular, code blocks with the `output` class have line comment markers inserted. Editors do not typically distinguish between code block classes, so some other visual indication is needed to separate them. This function is not based on a compliant Markdown parser and may give unpredictable results when used with invalid Markdown.

Equations

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

Instances For