structure Lean.Doc.MarkdownM.State : Type

The internal rendering state for MarkdownM.

• footnotes : Array (String × String)

@[reducible, inline]

abbrev Lean.Doc.MarkdownM (α : Type) : Type

The monad in which docstring Markdown is rendered. This is used when showing Verso docstrings as plain Markdown, such as in the language server.

Equations

• Lean.Doc.MarkdownM = StateRefT' IO.RealWorld Lean.Doc.MarkdownM.State Lean.CoreM

structure Lean.Doc.MarkdownM.InlineCtx : Type

Tracks which inline delimiters are already open so that nested * / ** / […](…) don't emit redundant openers and closers.

• inEmph : Bool

  The current code is inside emphasis (*…*).

• inBold : Bool

  The current code is inside strong emphasis (**…**).

• inLink : Bool

  The current code is inside a link's display text.

@[instance_reducible]

instance Lean.Doc.MarkdownM.instInhabitedInlineCtx : Inhabited InlineCtx

Equations

• Lean.Doc.MarkdownM.instInhabitedInlineCtx = { default := Lean.Doc.MarkdownM.instInhabitedInlineCtx.default }

def Lean.Doc.MarkdownM.run' (act : MarkdownM (Array String)) : CoreM String

Renders an action that produces an array of lines into a single Markdown string, appending any accumulated footnotes after the main body.

Equations

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

def Lean.Doc.prefixLines (p : String) (lines : Array String) : Array String

Applies a uniform prefix to every line. Empty lines receive the trimmed prefix to avoid trailing whitespace (which denotes a hard line break).

Equations

• Lean.Doc.prefixLines p lines = Array.map (fun (l : String) => if l.isEmpty = true then Lean.Doc.trimEndSpaces✝ p else p ++ l) lines

def Lean.Doc.prefixListLines (head rest : String) (lines : Array String) : Array String

Applies one prefix to the first line and a different prefix to subsequent lines. Used for list items, where the first line gets "* " / "1. " and the continuation lines get " " / " ".

Equations

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

def Lean.Doc.joinBlocks (blocks : Array (Array String)) : Array String

Concatenates an array of "block" line arrays into one line array, with a single empty separator line between adjacent non-empty blocks. Empty input blocks are skipped.

Equations

• Lean.Doc.joinBlocks blocks = Array.foldl (fun (acc b : Array String) => if b.isEmpty = true then acc else if acc.isEmpty = true then b else acc.push "" ++ b) #[] blocks

def Lean.Doc.joinInlines (parts : Array (Array String)) : Array String

Concatenates a array of lines, where each line is an array of rendered inlines. The last line of one piece is glued onto the first line of the next via glueInlineBoundary (so .text "a" followed by .text "b" yields one line "ab", but two adjacent .code spans get a U+200B between them).

Equations

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

class Lean.Doc.ToMarkdown (α : Type u) : Type u

A means of transforming values into Markdown lines.

• toMarkdown : α → MarkdownM (Array String)

  Render an α to its Markdown lines. The lines should not contain literal \n characters; line breaks are encoded by the array structure.

class Lean.Doc.MarkdownInline (i : Type u) : Type u

A way to transform inline elements extended with i into Markdown lines.

• toMarkdown : (Inline i → MarkdownM (Array String)) → i → Array (Inline i) → MarkdownM (Array String)

  Render the i and its contents to Markdown lines, given a recursive renderer for ordinary inline content.

@[instance_reducible]

instance Lean.Doc.instMarkdownInlineEmpty : MarkdownInline Empty

Equations

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

class Lean.Doc.MarkdownBlock (i : Type u) (b : Type v) : Type (max u v)

A way to transform block elements extended with b (containing inline elements extended with i) into Markdown lines.

• toMarkdown : (Inline i → MarkdownM (Array String)) → (Block i b → MarkdownM (Array String)) → b → Array (Block i b) → MarkdownM (Array String)

  Render the b and its contents to Markdown lines, given recursive renderers for inline and block content.

@[instance_reducible]

instance Lean.Doc.instMarkdownBlockEmpty {i : Type u_1} : MarkdownBlock i Empty

Equations

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

@[instance_reducible]

instance Lean.Doc.instToMarkdownInlineOfMarkdownInline {i : Type u_1} [MarkdownInline i] : ToMarkdown (Inline i)

Equations

• Lean.Doc.instToMarkdownInlineOfMarkdownInline = { toMarkdown := Lean.Doc.instToMarkdownInlineOfMarkdownInline._private_1 }

@[instance_reducible]

instance Lean.Doc.instToMarkdownBlockOfMarkdownInlineOfMarkdownBlock {i : Type u_1} {b : Type u_2} [MarkdownInline i] [MarkdownBlock i b] : ToMarkdown (Block i b)

Equations

• Lean.Doc.instToMarkdownBlockOfMarkdownInlineOfMarkdownBlock = { toMarkdown := Lean.Doc.instToMarkdownBlockOfMarkdownInlineOfMarkdownBlock._private_1 }

partial def Lean.Doc.partMarkdown {i : Type u_1} {b : Type u_2} {p : Type u_3} [MarkdownInline i] [MarkdownBlock i b] (level : Nat) (part : Part i b p) : MarkdownM (Array String)

Renders a Part (a logical document section) at the given heading level. Headings use ATX-style (#, ##, …) with level 0 rendering as #.

@[instance_reducible]

instance Lean.Doc.instToMarkdownPartOfMarkdownInlineOfMarkdownBlock {i : Type u_1} {b : Type u_2} {p : Type u_3} [MarkdownInline i] [MarkdownBlock i b] : ToMarkdown (Part i b p)

Equations

• Lean.Doc.instToMarkdownPartOfMarkdownInlineOfMarkdownBlock = { toMarkdown := fun (part : Lean.Doc.Part i b p) => Lean.Doc.partMarkdown 0 part }

@[reducible, inline]

abbrev Lean.Doc.InlineMdRendererOf (α : Type) : Type

A renderer for custom inline elements of type α. It receives a renderer for inline content, the custom element, and the element's fallback content.

Equations

• Lean.Doc.InlineMdRendererOf α = ((Lean.Doc.Inline Lean.ElabInline → Lean.Doc.MarkdownM (Array String)) → α → Array (Lean.Doc.Inline Lean.ElabInline) → Lean.Doc.MarkdownM (Array String))

@[reducible, inline]

abbrev Lean.Doc.BlockMdRendererOf (α : Type) : Type

A renderer for custom block elements of type α. It receives renderers for inline and block content, the custom element, and the element's fallback content.

Equations

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

@[reducible, inline]

abbrev Lean.Doc.InlineMdRenderer : Type

Renders a custom inline element to Markdown. It receives a renderer for inline content, the saved Dynamic description of the custom element, and the element's fallback content.

Equations

• Lean.Doc.InlineMdRenderer = Lean.Doc.InlineMdRendererOf Dynamic

@[reducible, inline]

abbrev Lean.Doc.BlockMdRenderer : Type

Renders a custom block element to Markdown. It receives renderers for inline and block content, the saved Dynamic description of the custom element, and the element's fallback content.

Equations

• Lean.Doc.BlockMdRenderer = Lean.Doc.BlockMdRendererOf Dynamic

def Lean.Doc.mkInlineMdRenderer (α : Type) [TypeName α] (f : InlineMdRendererOf α) : InlineMdRenderer

Wraps a typed inline renderer as an InlineMdRenderer by decoding the Dynamic custom element as α.

Equations

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

def Lean.Doc.mkBlockMdRenderer (α : Type) [TypeName α] (f : BlockMdRendererOf α) : BlockMdRenderer

Wraps a typed block renderer as a BlockMdRenderer by decoding the Dynamic custom element as α.

Equations

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

structure Lean.Doc.MdRendererState : Type

A set of registered Markdown renderers, keyed by custom element type names.

• imported : NameMap Name

  Renderers registered in imported modules.

• current : NameMap Name

  Renderers registered in the current module.

@[instance_reducible]

instance Lean.Doc.instInhabitedMdRendererState : Inhabited MdRendererState

Equations

• Lean.Doc.instInhabitedMdRendererState = { default := Lean.Doc.instInhabitedMdRendererState.default }

opaque Lean.Doc.docInlineMdExt : PersistentEnvExtension (Name × Name) (Name × Name) MdRendererState

Registry for custom inline element renderers that maps element type names to renderer names.

opaque Lean.Doc.docBlockMdExt : PersistentEnvExtension (Name × Name) (Name × Name) MdRendererState

Registry for custom block element renderers that maps element type names to renderer names.

def Lean.Doc.addBuiltinInlineMdRenderer (type : Name) (r : InlineMdRenderer) : IO Unit

Registers a builtin inline Markdown renderer.

Equations

• Lean.Doc.addBuiltinInlineMdRenderer type r = ST.Ref.modify Lean.Doc.builtinInlineMdRenderers✝ fun (x : Lean.NameMap Lean.Doc.InlineMdRenderer) => x.insert type r

def Lean.Doc.addBuiltinBlockMdRenderer (type : Name) (r : BlockMdRenderer) : IO Unit

Registers a builtin block Markdown renderer.

Equations

• Lean.Doc.addBuiltinBlockMdRenderer type r = ST.Ref.modify Lean.Doc.builtinBlockMdRenderers✝ fun (x : Lean.NameMap Lean.Doc.BlockMdRenderer) => x.insert type r

@[implemented_by _private.Lean.DocString.Markdown.0.Lean.Doc.inlineRendererForUnsafe]

opaque Lean.Doc.inlineRendererFor (typeName : Name) : CoreM (Option InlineMdRenderer)

Looks up the inline Markdown renderer registered for typeName, if any.

@[implemented_by _private.Lean.DocString.Markdown.0.Lean.Doc.blockRendererForUnsafe]

opaque Lean.Doc.blockRendererFor (typeName : Name) : CoreM (Option BlockMdRenderer)

Looks up the block Markdown renderer registered for typeName, if any.

def Lean.Doc.mdRendererHeartbeats : Nat

A small, fixed heartbeat budget applied afresh to each custom element renderer.

Docstrings are rendered constantly (e.g. on every hover), and renderers may run arbitrary MetaM, so this bounds the work any single element can impose.

Equations

• Lean.Doc.mdRendererHeartbeats = 200000

def Lean.Doc.withMdRendererBudget {α : Type} (x : MarkdownM α) : MarkdownM α

Runs an element renderer with a fresh mdRendererHeartbeats budget.

The budget applies to each renderer separately.

Equations

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

def Lean.Doc.withRendererFallback (fallback act : MarkdownM (Array String)) : MarkdownM (Array String)

Runs a renderer with a fallback.

If the renderer fails or exceeds its heartbeat budget, then the fallback content is rendered instead.

Equations

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

@[instance_reducible]

instance Lean.Doc.instMarkdownInlineElabInline : MarkdownInline ElabInline

Equations

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

@[instance_reducible]

instance Lean.Doc.instMarkdownBlockElabInlineElabBlock : MarkdownBlock ElabInline ElabBlock

Equations

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

@[instance_reducible]

instance Lean.Doc.instToMarkdownVersoDocString : ToMarkdown VersoDocString

Equations

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

@[instance_reducible]

instance Lean.Doc.instToMarkdownSnippet : ToMarkdown VersoModuleDocs.Snippet

Equations

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

def Lean.Doc.runMarkdown {α : Type} (env : Environment) (act : CoreM α) (options : Options := ∅) (currNamespace : Name := Name.anonymous) (openDecls : List OpenDecl := []) (cancelTk? : Option IO.CancelToken := none) : IO α

Runs a Markdown-rendering action against an environment, building a minimal CoreM context.

Equations

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

def Lean.findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin : Bool := true) (options : Options := ∅) (currNamespace : Name := Name.anonymous) (openDecls : List OpenDecl := []) (cancelTk? : Option IO.CancelToken := none) : IO (Option String)

Finds a docstring without performing any alias resolution or enrichment with extra metadata. The result is rendered as Markdown.

Docstrings to be shown to a user should be looked up with Lean.findDocString? instead.

Equations

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