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.

Equations

• Lean.Doc.MarkdownM = ReaderT Lean.Doc.MarkdownM.Context (StateM Lean.Doc.MarkdownM.State)

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

Generates Markdown, rendering the result from the final state.

Equations

• act.run context state = match act context state with | (val, state) => (val, Lean.Doc.MarkdownM.State.render✝ 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.

Equations

• act.run' context state = (act.run context state).snd

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

Adds a string to the current Markdown output.

Equations

• Lean.Doc.MarkdownM.push txt = modify fun (x : Lean.Doc.MarkdownM.State) => Lean.Doc.MarkdownM.State.push✝ x txt

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

Checks whether the current output ends with the given string.

Equations

• Lean.Doc.MarkdownM.endsWith txt = do let __do_lift ← get pure (Lean.Doc.MarkdownM.State.endsWith✝ __do_lift txt)

def Lean.Doc.MarkdownM.endBlock : MarkdownM Unit

Terminates the current block.

Equations

• Lean.Doc.MarkdownM.endBlock = modify fun (x : Lean.Doc.MarkdownM.State) => Lean.Doc.MarkdownM.State.endBlock✝ x

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

Increases the indentation level by one.

Equations

• Lean.Doc.MarkdownM.indent = withReader fun (st : Lean.Doc.MarkdownM.Context) => { inEmph := st.inEmph, inBold := st.inBold, inLink := st.inLink, linePrefix := st.linePrefix ++ " " }

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

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

Equations

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

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

Equations

• Lean.Doc.instToMarkdownInlineOfMarkdownInline = { toMarkdown := fun (inline : Lean.Doc.Inline i) => Lean.Doc.instToMarkdownInlineOfMarkdownInline._private_1 inline }

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

Equations

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

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

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