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.

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

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.

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

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

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.

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

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

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

@[instance_reducible]

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

@[instance_reducible]

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

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)

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

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

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

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

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

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

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

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

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

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.

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

Registers a builtin block Markdown renderer.

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

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

Runs an element renderer with a fresh mdRendererHeartbeats budget.

The budget applies to each renderer separately.

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.

@[instance_reducible]

instance Lean.Doc.instMarkdownInlineElabInline : MarkdownInline ElabInline

@[instance_reducible]

instance Lean.Doc.instMarkdownBlockElabInlineElabBlock : MarkdownBlock ElabInline ElabBlock

@[instance_reducible]

instance Lean.Doc.instToMarkdownVersoDocString : ToMarkdown VersoDocString

@[instance_reducible]

instance Lean.Doc.instToMarkdownSnippet : ToMarkdown VersoModuleDocs.Snippet

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.

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.