structure Lean.Doc.MarkdownM.Context : Type

The surrounding context of Markdown that's being generated, in order to prevent nestings that Markdown doesn't allow.

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

• linePrefix : String

  The prefix that should be added to each line (typically for indentation).

structure Lean.Doc.MarkdownM.State : Type

The state of a Markdown generation task.

• priorBlocks : String

  The blocks prior to the one being generated.

• currentBlock : String

  The block being generated.

• footnotes : Array (String × String)

  Footnotes

@[reducible, inline]

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

The monad for generating Markdown output.

def Lean.Doc.MarkdownM.run {α : Type} (act : MarkdownM α) (context : Context := { }) (state : State := { }) : α × String

Generates Markdown, rendering the result from the final state.

def Lean.Doc.MarkdownM.run' (act : MarkdownM Unit) (context : Context := { }) (state : State := { }) : String

Generates Markdown, rendering the result from the final state, without producing a value.

def Lean.Doc.MarkdownM.push (txt : String) : MarkdownM Unit

Adds a string to the current Markdown output.

def Lean.Doc.MarkdownM.endsWith (txt : String) : MarkdownM Bool

Checks whether the current output ends with the given string.

def Lean.Doc.MarkdownM.endBlock : MarkdownM Unit

Terminates the current block.

def Lean.Doc.MarkdownM.indent {α : Type} : MarkdownM α → MarkdownM α

Increases the indentation level by one.

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

A means of transforming values to Markdown representations.

• toMarkdown : α → MarkdownM Unit

  A function that transforms an α into a Markdown representation.

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

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

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

  A function that transforms an i and its contents into Markdown, given a way to transform the contents.

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 that contain inline elements extended with i into Markdown.

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

  A function that transforms a b and its contents into Markdown, given a way to transform the contents.

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

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

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

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)