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.
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.