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

Instances For

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

Instances For

source
instance Lean.Doc.instReprMathMode :
Repr MathMode
Equations

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

source
instance Lean.Doc.instBEqMathMode :
BEq MathMode
Equations

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

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

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

Instances For

source
instance Lean.Doc.instHashableMathMode :
Hashable MathMode
Equations

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

source
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

Instances For

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

- Lean.Doc.instOrdMathMode.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

Instances For

source
instance Lean.Doc.instOrdMathMode :
Ord MathMode
Equations

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

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

Instances For

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

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

source
partial def Lean.Doc.instBEqInline.beq {i✝ : Type u_1} [BEq i✝] :
Inline i✝ → Inline i✝ → Bool
source
instance Lean.Doc.instOrdInline {i✝ : Type u_1} [Ord i✝] :
Ord (Inline i✝)
Equations

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

source
partial def Lean.Doc.instOrdInline.ord {i✝ : Type u_1} [Ord i✝] :
Inline i✝ → Inline i✝ → Ordering
source
instance Lean.Doc.instReprInline {i✝ : Type u_1} [Repr i✝] :
Repr (Inline i✝)
Equations

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

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

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

Instances For

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

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

source
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

Instances For

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

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

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

No inline content.

Equations

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

Instances For

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

Instances For

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

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

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

Instances For

source
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

Instances For

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

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

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

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

source
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

Instances For

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

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

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

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

Instances For

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

Instances For

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

Instances For

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

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

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

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

source
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

Instances For

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

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

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

Instances For

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

Instances For

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

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

Instances For

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

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

source
partial def Lean.Doc.instReprBlock.repr {i✝ : Type u_1} {b✝ : Type u_2} [Repr i✝] [Repr b✝] :
Block i✝ b✝ → Nat → Format
source
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 }

source
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

Instances For

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

source
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 #[]

Instances For

source
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

Instances For

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

Instances For

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

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

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

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

Instances For

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

source
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

Instances For