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

Equations

• Lean.Doc.instReprMathMode.repr Lean.Doc.MathMode.inline prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.Doc.MathMode.inline")).group prec✝
• Lean.Doc.instReprMathMode.repr Lean.Doc.MathMode.display prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.Doc.MathMode.display")).group prec✝

instance Lean.Doc.instReprMathMode : Repr MathMode

Equations

• Lean.Doc.instReprMathMode = { reprPrec := Lean.Doc.instReprMathMode.repr }

instance Lean.Doc.instBEqMathMode : BEq MathMode

Equations

• Lean.Doc.instBEqMathMode = { beq := Lean.Doc.instBEqMathMode.beq }

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

Equations

• Lean.Doc.instBEqMathMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

Equations

• Lean.Doc.instHashableMathMode.hash Lean.Doc.MathMode.inline = 0
• Lean.Doc.instHashableMathMode.hash Lean.Doc.MathMode.display = 1

instance Lean.Doc.instHashableMathMode : Hashable MathMode

Equations

• Lean.Doc.instHashableMathMode = { hash := Lean.Doc.instHashableMathMode.hash }

instance Lean.Doc.instOrdMathMode : Ord MathMode

Equations

• Lean.Doc.instOrdMathMode = { compare := Lean.Doc.instOrdMathMode.ord }

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

Equations

• Lean.Doc.instOrdMathMode.ord Lean.Doc.MathMode.inline Lean.Doc.MathMode.inline = Ordering.eq
• Lean.Doc.instOrdMathMode.ord Lean.Doc.MathMode.inline x✝ = Ordering.lt
• Lean.Doc.instOrdMathMode.ord x Lean.Doc.MathMode.inline = Ordering.gt
• Lean.Doc.instOrdMathMode.ord Lean.Doc.MathMode.display Lean.Doc.MathMode.display = Ordering.eq

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.

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

Equations

• Lean.Doc.instBEqInline = { beq := Lean.Doc.instBEqInline.beq }

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

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

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

Equations

• Lean.Doc.instOrdInline = { compare := Lean.Doc.instOrdInline.ord }

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

Equations

• Lean.Doc.instReprInline = { reprPrec := Lean.Doc.instReprInline.repr }

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

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

Equations

• Lean.Doc.instInhabitedInline = { default := Lean.Doc.instInhabitedInline.default }

def Lean.Doc.instInhabitedInline.default {a✝ : Type u_1} : Inline a✝

Equations

• Lean.Doc.instInhabitedInline.default = Lean.Doc.Inline.text default

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.

Equations

• Lean.Doc.Inline.cast inlines_eq x = inlines_eq ▸ x

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

Equations

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

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

No inline content.

Equations

• Lean.Doc.Inline.empty = Lean.Doc.Inline.concat #[]

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 Lean.Doc.instReprListItem {α✝ : Type u_1} [Repr α✝] : Repr (ListItem α✝)

Equations

• Lean.Doc.instReprListItem = { reprPrec := Lean.Doc.instReprListItem.repr }

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

Equations

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

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

Equations

• Lean.Doc.instBEqListItem.beq { contents := a } { contents := b } = (a == b)
• Lean.Doc.instBEqListItem.beq x✝¹ x✝ = false

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

Equations

• Lean.Doc.instBEqListItem = { beq := Lean.Doc.instBEqListItem.beq }

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

Equations

• Lean.Doc.instOrdListItem.ord { contents := a } { contents := b } = (compare a b).then Ordering.eq

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

Equations

• Lean.Doc.instOrdListItem = { compare := Lean.Doc.instOrdListItem.ord }

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

Equations

• Lean.Doc.instInhabitedListItem = { default := Lean.Doc.instInhabitedListItem.default }

def Lean.Doc.instInhabitedListItem.default {a✝ : Type u_1} : ListItem a✝

Equations

• Lean.Doc.instInhabitedListItem.default = { contents := default }

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.

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

Equations

• Lean.Doc.instReprDescItem = { reprPrec := Lean.Doc.instReprDescItem.repr }

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

Equations

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

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

Equations

• Lean.Doc.instBEqDescItem = { beq := Lean.Doc.instBEqDescItem.beq }

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

Equations

• Lean.Doc.instBEqDescItem.beq { term := a, desc := a_1 } { term := b, desc := b_1 } = (a == b && a_1 == b_1)
• Lean.Doc.instBEqDescItem.beq x✝¹ x✝ = false

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

Equations

• Lean.Doc.instOrdDescItem.ord { term := a, desc := a_1 } { term := b, desc := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

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

Equations

• Lean.Doc.instOrdDescItem = { compare := Lean.Doc.instOrdDescItem.ord }

def Lean.Doc.instInhabitedDescItem.default {a✝ : Type u_1} {a✝¹ : Type u_2} : DescItem a✝ a✝¹

Equations

• Lean.Doc.instInhabitedDescItem.default = { term := default, desc := default }

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

Equations

• Lean.Doc.instInhabitedDescItem = { default := Lean.Doc.instInhabitedDescItem.default }

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.

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

Equations

• Lean.Doc.instBEqBlock = { beq := Lean.Doc.instBEqBlock.beq }

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

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 Lean.Doc.instOrdBlock {i✝ : Type u_1} {b✝ : Type u_2} [Ord i✝] [Ord b✝] : Ord (Block i✝ b✝)

Equations

• Lean.Doc.instOrdBlock = { compare := Lean.Doc.instOrdBlock.ord }

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

Equations

• Lean.Doc.instReprBlock = { reprPrec := Lean.Doc.instReprBlock.repr }

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

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

Equations

• Lean.Doc.instInhabitedBlock = { default := Lean.Doc.instInhabitedBlock.default }

def Lean.Doc.instInhabitedBlock.default {a✝ : Type u_1} {a✝¹ : Type u_2} : Block a✝ a✝¹

Equations

• Lean.Doc.instInhabitedBlock.default = Lean.Doc.Block.para default

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

An empty block with no content.

Equations

• Lean.Doc.Block.empty = Lean.Doc.Block.concat #[]

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.

Equations

• Lean.Doc.Block.cast inlines_eq blocks_eq x = inlines_eq ▸ blocks_eq ▸ x

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)

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

Equations

• Lean.Doc.instBEqPart = { beq := Lean.Doc.instBEqPart.beq }

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

Equations

• Lean.Doc.instOrdPart = { compare := Lean.Doc.instOrdPart.ord }

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

Equations

• Lean.Doc.instReprPart = { reprPrec := Lean.Doc.instReprPart.repr }

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 Lean.Doc.instInhabitedPart {a✝ : Type u_1} {a✝¹ : Type u_2} {a✝² : Type u_3} : Inhabited (Part a✝ a✝¹ a✝²)

Equations

• Lean.Doc.instInhabitedPart = { default := Lean.Doc.instInhabitedPart.default }

def Lean.Doc.instInhabitedPart.default {a✝ : Type u_1} {a✝¹ : Type u_2} {a✝² : Type u_3} : Part a✝ a✝¹ a✝²

Equations

• Lean.Doc.instInhabitedPart.default = { title := default, titleString := default, metadata := default, content := default, subParts := default }

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.

Equations

• Lean.Doc.Part.cast inlines_eq blocks_eq metadata_eq x = inlines_eq ▸ blocks_eq ▸ metadata_eq ▸ x