inductive Lean.Doc.MathMode : Type

How to render mathematical content.

• inline : MathMode

  The math content is part of the text flow.

• display : MathMode

  The math content is set apart from the text flow, with more space.

def Lean.Doc.instReprMathMode.repr : MathMode → Nat → Format

@[instance_reducible]

instance Lean.Doc.instReprMathMode : Repr MathMode

@[instance_reducible]

instance Lean.Doc.instBEqMathMode : BEq MathMode

def Lean.Doc.instBEqMathMode.beq : MathMode → MathMode → Bool

def Lean.Doc.instHashableMathMode.hash : MathMode → UInt64

@[instance_reducible]

instance Lean.Doc.instHashableMathMode : Hashable MathMode

@[instance_reducible]

instance Lean.Doc.instOrdMathMode : Ord MathMode

def Lean.Doc.instOrdMathMode.ord : MathMode → MathMode → Ordering

inductive Lean.Doc.Inline (i : Type u) : Type u

Inline content that is part of the text flow.

• text {i : Type u} (string : String) : Inline i

  Textual content.

• emph {i : Type u} (content : Array (Inline i)) : Inline i

  Emphasis, typically rendered using italic text.

• bold {i : Type u} (content : Array (Inline i)) : Inline i

  Strong emphasis, typically rendered using bold text.

• code {i : Type u} (string : String) : Inline i

  Inline literal code, typically rendered in a monospace font.

• math {i : Type u} (mode : MathMode) (string : String) : Inline i

  Embedded TeX math, to be rendered by an engine such as TeX or KaTeX. The mode determines whether it is rendered in inline mode or display mode; even display-mode math is an inline element for purposes of document structure.

• linebreak {i : Type u} (string : String) : Inline i

  A user's line break. These are typically ignored when rendering, but don't need to be.

• link {i : Type u} (content : Array (Inline i)) (url : String) : Inline i

  A link to some URL.

• footnote {i : Type u} (name : String) (content : Array (Inline i)) : Inline i

  A footnote. In Verso's concrete syntax, their contents are specified elsewhere, but elaboration places the contents at the use site.

• image {i : Type u} (alt url : String) : Inline i

  An image. alt should be displayed if the image can't be shown.

• concat {i : Type u} (content : Array (Inline i)) : Inline i

  A sequence of inline elements.

• other {i : Type u} (container : i) (content : Array (Inline i)) : Inline i

  A genre-specific inline element. container specifies what kind of element it is, and content specifies the contained elements.

partial def Lean.Doc.instBEqInline.beq {i✝ : Type u_1} [BEq i✝] : Inline i✝ → Inline i✝ → Bool

@[instance_reducible]

instance Lean.Doc.instBEqInline {i✝ : Type u_1} [BEq i✝] : BEq (Inline i✝)

partial def Lean.Doc.instOrdInline.ord {i✝ : Type u_1} [Ord i✝] : Inline i✝ → Inline i✝ → Ordering

@[instance_reducible]

instance Lean.Doc.instOrdInline {i✝ : Type u_1} [Ord i✝] : Ord (Inline i✝)

@[instance_reducible]

instance Lean.Doc.instReprInline {i✝ : Type u_1} [Repr i✝] : Repr (Inline i✝)

partial def Lean.Doc.instReprInline.repr {i✝ : Type u_1} [Repr i✝] : Inline i✝ → Nat → Format

@[instance_reducible]

instance Lean.Doc.instInhabitedInline {a✝ : Type u_1} : Inhabited (Inline a✝)

def Lean.Doc.Inline.cast {i i' : Type u_1} (inlines_eq : i = i') (x : Inline i) : Inline i'

Rewrites using a proof that two inline element types are equal.

@[instance_reducible]

instance Lean.Doc.instAppendInline {i : Type u_1} : Append (Inline i)

def Lean.Doc.Inline.empty {i : Type u_1} : Inline i

No inline content.

structure Lean.Doc.ListItem (α : Type u) : Type u

An item in either an ordered or unordered list.

• contents : Array α

  The contents of the list item.

@[instance_reducible]

instance Lean.Doc.instReprListItem {α✝ : Type u_1} [Repr α✝] : Repr (ListItem α✝)

def Lean.Doc.instReprListItem.repr {α✝ : Type u_1} [Repr α✝] : ListItem α✝ → Nat → Format

def Lean.Doc.instBEqListItem.beq {α✝ : Type u_1} [BEq α✝] : ListItem α✝ → ListItem α✝ → Bool

@[instance_reducible]

instance Lean.Doc.instBEqListItem {α✝ : Type u_1} [BEq α✝] : BEq (ListItem α✝)

@[instance_reducible]

instance Lean.Doc.instOrdListItem {α✝ : Type u_1} [Ord α✝] : Ord (ListItem α✝)

def Lean.Doc.instOrdListItem.ord {α✝ : Type u_1} [Ord α✝] : ListItem α✝ → ListItem α✝ → Ordering

@[instance_reducible]

instance Lean.Doc.instInhabitedListItem {a✝ : Type u_1} : Inhabited (ListItem a✝)

structure Lean.Doc.DescItem (α : Type u) (β : Type v) : Type (max u v)

An item in a description list.

• term : Array α

  The term being described.

• desc : Array β

  The description itself.

def Lean.Doc.instReprDescItem.repr {α✝ : Type u_1} {β✝ : Type u_2} [Repr α✝] [Repr β✝] : DescItem α✝ β✝ → Nat → Format

@[instance_reducible]

instance Lean.Doc.instReprDescItem {α✝ : Type u_1} {β✝ : Type u_2} [Repr α✝] [Repr β✝] : Repr (DescItem α✝ β✝)

@[instance_reducible]

instance Lean.Doc.instBEqDescItem {α✝ : Type u_1} {β✝ : Type u_2} [BEq α✝] [BEq β✝] : BEq (DescItem α✝ β✝)

def Lean.Doc.instBEqDescItem.beq {α✝ : Type u_1} {β✝ : Type u_2} [BEq α✝] [BEq β✝] : DescItem α✝ β✝ → DescItem α✝ β✝ → Bool

@[instance_reducible]

instance Lean.Doc.instOrdDescItem {α✝ : Type u_1} {β✝ : Type u_2} [Ord α✝] [Ord β✝] : Ord (DescItem α✝ β✝)

def Lean.Doc.instOrdDescItem.ord {α✝ : Type u_1} {β✝ : Type u_2} [Ord α✝] [Ord β✝] : DescItem α✝ β✝ → DescItem α✝ β✝ → Ordering

@[instance_reducible]

instance Lean.Doc.instInhabitedDescItem {a✝ : Type u_1} {a✝¹ : Type u_2} : Inhabited (DescItem a✝ a✝¹)

inductive Lean.Doc.Block (i : Type u) (b : Type v) : Type (max u v)

Block-level content in a document.

• para {i : Type u} {b : Type v} (contents : Array (Inline i)) : Block i b

  A paragraph.

• code {i : Type u} {b : Type v} (content : String) : Block i b

  A code block.

• ul {i : Type u} {b : Type v} (items : Array (ListItem (Block i b))) : Block i b

  An unordered list.

• ol {i : Type u} {b : Type v} (start : Int) (items : Array (ListItem (Block i b))) : Block i b

  An ordered list.

• dl {i : Type u} {b : Type v} (items : Array (DescItem (Inline i) (Block i b))) : Block i b

  A description list that associates explanatory text with shorter items.

• blockquote {i : Type u} {b : Type v} (items : Array (Block i b)) : Block i b

  A quotation.

• concat {i : Type u} {b : Type v} (content : Array (Block i b)) : Block i b

  Multiple blocks, merged.

• other {i : Type u} {b : Type v} (container : b) (content : Array (Block i b)) : Block i b

  A genre-specific block. container specifies what kind of block it is, while content specifies the content within the block.

partial def Lean.Doc.instBEqBlock.beq {i✝ : Type u_1} {b✝ : Type u_2} [BEq i✝] [BEq b✝] : Block i✝ b✝ → Block i✝ b✝ → Bool

@[instance_reducible]

instance Lean.Doc.instBEqBlock {i✝ : Type u_1} {b✝ : Type u_2} [BEq i✝] [BEq b✝] : BEq (Block i✝ b✝)

@[instance_reducible]

instance Lean.Doc.instOrdBlock {i✝ : Type u_1} {b✝ : Type u_2} [Ord i✝] [Ord b✝] : Ord (Block i✝ b✝)

partial def Lean.Doc.instOrdBlock.ord {i✝ : Type u_1} {b✝ : Type u_2} [Ord i✝] [Ord b✝] : Block i✝ b✝ → Block i✝ b✝ → Ordering

@[instance_reducible]

instance Lean.Doc.instReprBlock {i✝ : Type u_1} {b✝ : Type u_2} [Repr i✝] [Repr b✝] : Repr (Block i✝ b✝)

partial def Lean.Doc.instReprBlock.repr {i✝ : Type u_1} {b✝ : Type u_2} [Repr i✝] [Repr b✝] : Block i✝ b✝ → Nat → Format

@[instance_reducible]

instance Lean.Doc.instInhabitedBlock {a✝ : Type u_1} {a✝¹ : Type u_2} : Inhabited (Block a✝ a✝¹)

def Lean.Doc.Block.empty {i : Type u_1} {b : Type u_2} : Block i b

An empty block with no content.

def Lean.Doc.Block.cast {i i' : Type u_1} {b b' : Type u_2} (inlines_eq : i = i') (blocks_eq : b = b') (x : Block i b) : Block i' b'

Rewrites using proofs that two inline element types and two block types are equal.

structure Lean.Doc.Part (i : Type u) (b : Type v) (p : Type w) : Type (max u v w)

A logical division of a document.

• title : Array (Inline i)

  The part's title

• titleString : String

  A string approximation of the part's title, for use in contexts where formatted text is invalid.

• metadata : Option p

  Genre-specific metadata

• content : Array (Block i b)

  The part's textual content

• subParts : Array (Part i b p)

  Sub-parts (e.g. subsections of a section, sections of a chapter)

partial def Lean.Doc.instBEqPart.beq {i✝ : Type u_1} {b✝ : Type u_2} {p✝ : Type u_3} [BEq i✝] [BEq b✝] [BEq p✝] : Part i✝ b✝ p✝ → Part i✝ b✝ p✝ → Bool

@[instance_reducible]

instance Lean.Doc.instBEqPart {i✝ : Type u_1} {b✝ : Type u_2} {p✝ : Type u_3} [BEq i✝] [BEq b✝] [BEq p✝] : BEq (Part i✝ b✝ p✝)

@[instance_reducible]

instance Lean.Doc.instOrdPart {i✝ : Type u_1} {b✝ : Type u_2} {p✝ : Type u_3} [Ord i✝] [Ord b✝] [Ord p✝] : Ord (Part i✝ b✝ p✝)

partial def Lean.Doc.instOrdPart.ord {i✝ : Type u_1} {b✝ : Type u_2} {p✝ : Type u_3} [Ord i✝] [Ord b✝] [Ord p✝] : Part i✝ b✝ p✝ → Part i✝ b✝ p✝ → Ordering

@[instance_reducible]

instance Lean.Doc.instReprPart {i✝ : Type u_1} {b✝ : Type u_2} {p✝ : Type u_3} [Repr i✝] [Repr b✝] [Repr p✝] : Repr (Part i✝ b✝ p✝)

partial def Lean.Doc.instReprPart.repr {i✝ : Type u_1} {b✝ : Type u_2} {p✝ : Type u_3} [Repr i✝] [Repr b✝] [Repr p✝] : Part i✝ b✝ p✝ → Nat → Format

@[instance_reducible]

instance Lean.Doc.instInhabitedPart {a✝ : Type u_1} {a✝¹ : Type u_2} {a✝² : Type u_3} : Inhabited (Part a✝ a✝¹ a✝²)

def Lean.Doc.Part.cast {i i' : Type u_1} {b b' : Type u_2} {p p' : Type u_3} (inlines_eq : i = i') (blocks_eq : b = b') (metadata_eq : p = p') (x : Part i b p) : Part i' b' p'

Rewrites using proofs that inline element types, block types, and metadata types are equal.

@[reducible, inline]

abbrev Lean.Doc.VersoDocument : Type

A Verso document, which is a sequence of blocks. Its syntax is produced by Lean.Doc.Parser.document.

Use VersoDocument.view or TSyntax.getVersoBlocks to extract its contents.