@[reducible, inline]

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

A monad for accumulating footnotes while rendering Markdown. Footnote labels are paired with their already-rendered bodies, in order of first reference. MarkdownM.run' flushes them at the end of the document.

Equations

• Lean.Doc.MarkdownM = StateM (Array (String × String))

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.

@[implicit_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)) : 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.

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

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

@[implicit_reducible]

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

Equations

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

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

@[implicit_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 }