Lean.DocString.Types

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

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

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

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

Instances For

source

instance Lean.Doc.instInhabitedInline {a✝ : Type u_1} :

Inhabited (Inline a✝)

Equations

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

Instances For

source

instance Lean.Doc.instAppendInline {i : Type u_1} :

Append (Inline i)

Equations

source

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

Inline i

No inline content.

Equations

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

source

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

ListItem α✝ → Nat → Format

Equations

Instances For

source

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

ListItem α✝ → ListItem α✝ → Bool

Equations

Instances For

source

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

BEq (ListItem α✝)

Equations

source

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

Ord (ListItem α✝)

Equations

source

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

ListItem α✝ → ListItem α✝ → Ordering

Equations

Instances For

source

instance Lean.Doc.instInhabitedListItem {a✝ : Type u_1} :

Inhabited (ListItem a✝)

Equations

source

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

ListItem a✝

Equations

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

Instances For

source

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

Repr (DescItem α✝ β✝)

Equations

source

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

BEq (DescItem α✝ β✝)

Equations

source

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

DescItem α✝ β✝ → DescItem α✝ β✝ → Bool

Equations

Instances For

source

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

Ord (DescItem α✝ β✝)

Equations

source

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

DescItem α✝ β✝ → DescItem α✝ β✝ → Ordering

Equations

Instances For

source

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

DescItem a✝ a✝¹

Equations

Instances For

source

instance Lean.Doc.instInhabitedDescItem {a✝ : Type u_1} {a✝¹ : Type u_2} :

Inhabited (DescItem a✝ a✝¹)

Equations

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

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

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

source

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

Block a✝ a✝¹

Equations

Instances For

source

instance Lean.Doc.instInhabitedBlock {a✝ : Type u_1} {a✝¹ : Type u_2} :

Inhabited (Block a✝ a✝¹)

Equations

source

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

Block i b

An empty block with no content.

Equations

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

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

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

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

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

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

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

Instances For