This module declares the syntax of Verso documents.

The concrete syntax falls outside what Lean's parsing framework can express, so Verso has a separate parser, in Lean.DocString.Parser, written with the lower-level parts of Lean's parser. The node kinds it produces are declared here, in Lean.Doc.Parser, together with the tokens that store literal content and the accessors that decode them.

Consumers read this syntax through the views in Lean.DocString.View, which is the only place that matches document syntax directly.

Elaboration turns a parsed document into Lean syntax for the Verso document AST of Lean.DocString.Types, and may invoke user-written metaprograms on the way: the concrete syntax is not extensible, but roles, directives, and code blocks are hooks for extension. That step is in Lean.Elab.DocString.

The tokens that store literal Verso content. The Verso parser builds them itself, so each declaration below supplies only the antiquotation that can be used in Lean syntax quasiquotations. Its own name is the token's syntax node kind.

def Lean.Doc.Parser.versoText : Parser.Parser

Literal text content.

Equations

• Lean.Doc.Parser.versoText = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.mkAntiquot "versoText" `Lean.Doc.Parser.versoText

def Lean.Doc.Parser.versoRef : Parser.Parser

The name of a footnote or a link reference.

Equations

• Lean.Doc.Parser.versoRef = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.mkAntiquot "versoRef" `Lean.Doc.Parser.versoRef

def Lean.Doc.Parser.versoLinkUrl : Parser.Parser

The URL of a link or an image.

Equations

• Lean.Doc.Parser.versoLinkUrl = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.mkAntiquot "versoLinkUrl" `Lean.Doc.Parser.versoLinkUrl

def Lean.Doc.Parser.versoLinkRefUrl : Parser.Parser

The URL that a link reference definition provides.

Equations

• Lean.Doc.Parser.versoLinkRefUrl = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.mkAntiquot "versoLinkRefUrl" `Lean.Doc.Parser.versoLinkRefUrl

def Lean.Doc.Parser.versoImageAlt : Parser.Parser

The alternate text of an image.

Equations

• Lean.Doc.Parser.versoImageAlt = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.mkAntiquot "versoImageAlt" `Lean.Doc.Parser.versoImageAlt

def Lean.Doc.Parser.versoCode : Parser.Parser

Literal inline code content.

Equations

• Lean.Doc.Parser.versoCode = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.mkAntiquot "versoCode" `Lean.Doc.Parser.versoCode

def Lean.Doc.Parser.versoCodeLine : Parser.Parser

One source line of inline code or code block content.

Equations

• Lean.Doc.Parser.versoCodeLine = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.mkAntiquot "versoCodeLine" `Lean.Doc.Parser.versoCodeLine

def Lean.Doc.Parser.versoCodeBlock : Parser.Parser

Literal code block content.

Equations

• Lean.Doc.Parser.versoCodeBlock = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.mkAntiquot "versoCodeBlock" `Lean.Doc.Parser.versoCodeBlock

The kinds of the tokens that store literal content, and the TSyntax types over them. A token contains the source text exactly as written, keeping escape sequences, boundary spaces, and indentation. The getVerso* accessors decode it.

def Lean.Doc.versoTextKind : SyntaxNodeKind

Tokens that contain Verso text content.

Equations

• Lean.Doc.versoTextKind = `Lean.Doc.Parser.versoText

def Lean.Doc.versoRefKind : SyntaxNodeKind

The name of a Verso footnote or link reference name.

Equations

• Lean.Doc.versoRefKind = `Lean.Doc.Parser.versoRef

def Lean.Doc.versoLinkUrlKind : SyntaxNodeKind

The URL of a Verso link or image.

Equations

• Lean.Doc.versoLinkUrlKind = `Lean.Doc.Parser.versoLinkUrl

def Lean.Doc.versoLinkRefUrlKind : SyntaxNodeKind

The URL that a Verso link reference definition provides.

Equations

• Lean.Doc.versoLinkRefUrlKind = `Lean.Doc.Parser.versoLinkRefUrl

def Lean.Doc.versoImageAltKind : SyntaxNodeKind

The alternate text of a Verso image.

Equations

• Lean.Doc.versoImageAltKind = `Lean.Doc.Parser.versoImageAlt

def Lean.Doc.versoCodeKind : SyntaxNodeKind

The contents of Verso inline code.

Equations

• Lean.Doc.versoCodeKind = `Lean.Doc.Parser.versoCode

def Lean.Doc.versoCodeLineKind : SyntaxNodeKind

One source line inside Verso inline code or a Verso code block.

Equations

• Lean.Doc.versoCodeLineKind = `Lean.Doc.Parser.versoCodeLine

def Lean.Doc.versoCodeBlockKind : SyntaxNodeKind

The contents of a Verso code block.

Equations

• Lean.Doc.versoCodeBlockKind = `Lean.Doc.Parser.versoCodeBlock

def Lean.Doc.parseFailureKind : SyntaxNodeKind

The text of a Verso docstring whose markup does not parse.

Equations

• Lean.Doc.parseFailureKind = `Lean.Doc.Parser.parseFailure

@[reducible, inline]

abbrev Lean.Doc.VersoText : Type

Text content in a Verso document. The token contains the source text with escape sequences intact. Use VersoText.view or TSyntax.getVersoText to decode it.

Equations

• Lean.Doc.VersoText = Lean.TSyntax `Lean.Doc.Parser.versoText

@[reducible, inline]

abbrev Lean.Doc.VersoRefName : Type

The name of a footnote or a link reference in a Verso document. Use VersoRefName.view or TSyntax.getVersoRefName to decode its name to a string.

Equations

• Lean.Doc.VersoRefName = Lean.TSyntax `Lean.Doc.Parser.versoRef

@[reducible, inline]

abbrev Lean.Doc.VersoLinkUrl : Type

The URL of a link or an image in a Verso document. Use VersoLinkUrl.view or TSyntax.getVersoLinkUrl to decode the URL to a string.

Equations

• Lean.Doc.VersoLinkUrl = Lean.TSyntax `Lean.Doc.Parser.versoLinkUrl

@[reducible, inline]

abbrev Lean.Doc.VersoLinkRefUrl : Type

The URL that a link reference definition provides in a Verso document. Use VersoLinkRefUrl.view or TSyntax.getVersoLinkRefUrl to decode the URL to a string.

Equations

• Lean.Doc.VersoLinkRefUrl = Lean.TSyntax `Lean.Doc.Parser.versoLinkRefUrl

@[reducible, inline]

abbrev Lean.Doc.VersoImageAlt : Type

The alternate text of an image in a Verso document. Use VersoImageAlt.view or TSyntax.getVersoImageAlt to decode the alternate text to a string.

Equations

• Lean.Doc.VersoImageAlt = Lean.TSyntax `Lean.Doc.Parser.versoImageAlt

@[reducible, inline]

abbrev Lean.Doc.VersoCode : Type

Inline code content in a Verso document, with one versoCodeLine token per source line. Use VersoCode.view or TSyntax.getVersoCode to decode it to a string.

Equations

• Lean.Doc.VersoCode = Lean.TSyntax `Lean.Doc.Parser.versoCode

@[reducible, inline]

abbrev Lean.Doc.VersoCodeLine : Type

A single source line of code content in a Verso document, inside inline code or a code block. Only indentation that is semantically part of the line of code is included in the atom, while indentation of a code block or docstring as a whole is part of the tokens' whitespace.

Use VersoCodeLine.view or TSyntax.getVersoCodeLine to decode the line to a string.

Equations

• Lean.Doc.VersoCodeLine = Lean.TSyntax `Lean.Doc.Parser.versoCodeLine

@[reducible, inline]

abbrev Lean.Doc.VersoCodeBlock : Type

Code block content in a Verso document, with one versoCodeLine token per source line. The code block's indentation is whitespace between tokens. Use VersoCodeBlock.view or TSyntax.getVersoCodeBlock to decode it to a string.

Equations

• Lean.Doc.VersoCodeBlock = Lean.TSyntax `Lean.Doc.Parser.versoCodeBlock

def Lean.Doc.longestBacktickRun (str : String) : Nat

The length of the longest run of backticks in str. A delimiter of inline code, and the fence of a code block, is longer than every run of backticks in the content it surrounds.

Equations

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

def Lean.Doc.versoCodeBoundarySpaces (str : String) : Bool

Whether str begins and ends with a space and contains a character other than a space.

In a code element, this sequence denotes the content with a space removed from each end. The parser records those two spaces as whitespace rather than content.

Equations

• Lean.Doc.versoCodeBoundarySpaces str = (str.startsWith " " && str.endsWith " " && str.any fun (x : Char) => x != ' ')

def Lean.Doc.escapeVersoLinkUrl (value : String) : String

Escapes value so that getVersoLinkUrl reads it back unchanged.

Equations

• Lean.Doc.escapeVersoLinkUrl value = Lean.Doc.escapeVersoDelimited✝ [')'] value

def Lean.Doc.escapeVersoImageAlt (value : String) : String

Escapes value so that getVersoImageAlt reads it back unchanged.

Equations

• Lean.Doc.escapeVersoImageAlt value = Lean.Doc.escapeVersoDelimited✝ [']'] value

def Lean.TSyntax.getVersoText (s : Doc.VersoText) : String

Decodes the text that a Verso text token denotes, interpreting escape sequences.

Equations

• Lean.TSyntax.getVersoText s = Lean.Doc.unescapeVerso✝ ((Lean.Syntax.isLit? Lean.Doc.versoTextKind s.raw).getD "")

def Lean.TSyntax.getVersoTextSource (s : Doc.VersoText) : String

Returns the text of a Verso text token as it was written, with its escape sequences intact.

Equations

• Lean.TSyntax.getVersoTextSource s = (Lean.Syntax.isLit? Lean.Doc.versoTextKind s.raw).getD ""

def Lean.TSyntax.getVersoRefName (s : Doc.VersoRefName) : String

Decodes the name that a Verso footnote or link reference token contains.

Equations

• Lean.TSyntax.getVersoRefName s = (Lean.Syntax.isLit? Lean.Doc.versoRefKind s.raw).getD ""

def Lean.TSyntax.getVersoLinkUrl (s : Doc.VersoLinkUrl) : String

Decodes the URL that a Verso link or image token contains, interpreting escape sequences.

Equations

• Lean.TSyntax.getVersoLinkUrl s = Lean.Doc.unescapeVerso✝ ((Lean.Syntax.isLit? Lean.Doc.versoLinkUrlKind s.raw).getD "")

def Lean.TSyntax.getVersoLinkRefUrl (s : Doc.VersoLinkRefUrl) : String

Returns the URL that a Verso link reference definition token contains. These positions do not support escape sequences.

Equations

• Lean.TSyntax.getVersoLinkRefUrl s = (Lean.Syntax.isLit? Lean.Doc.versoLinkRefUrlKind s.raw).getD ""

def Lean.TSyntax.getVersoImageAlt (s : Doc.VersoImageAlt) : String

Decodes the alternate text that a Verso image token contains, interpreting escape sequences.

Equations

• Lean.TSyntax.getVersoImageAlt s = Lean.Doc.unescapeVerso✝ ((Lean.Syntax.isLit? Lean.Doc.versoImageAltKind s.raw).getD "")

def Lean.TSyntax.getVersoCodeLine (s : Doc.VersoCodeLine) : String

Returns the text of one source line inside Verso inline code or a Verso code block.

Equations

• Lean.TSyntax.getVersoCodeLine s = (Lean.Syntax.isLit? Lean.Doc.versoCodeLineKind s.raw).getD ""

def Lean.TSyntax.getVersoCodeLines (s : Doc.VersoCode) : TSyntaxArray `Lean.Doc.Parser.versoCodeLine

Returns the source lines of Verso inline code, in order.

Equations

• Lean.TSyntax.getVersoCodeLines s = Lean.TSyntaxArray.mk s.raw[0].getArgs

def Lean.TSyntax.getVersoCode (s : Doc.VersoCode) : String

Returns the code that Verso inline code content denotes, which is the text of its lines in order.

Equations

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

def Lean.TSyntax.getVersoCodeBlockLines (s : Doc.VersoCodeBlock) : TSyntaxArray `Lean.Doc.Parser.versoCodeLine

Returns the source lines of a Verso code block, in order.

Equations

• Lean.TSyntax.getVersoCodeBlockLines s = Lean.TSyntaxArray.mk s.raw[0].getArgs

def Lean.TSyntax.getVersoCodeBlock (s : Doc.VersoCodeBlock) : String

Returns the contents of a Verso code block, which are the texts of its lines in order.

Equations

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

def Lean.Doc.VersoText.view (s : VersoText) : String

Decodes the text that a Verso text token denotes, interpreting escape sequences.

Equations

• s.view = Lean.TSyntax.getVersoText s

def Lean.Doc.VersoRefName.view (s : VersoRefName) : String

Decodes the name that a Verso footnote or link reference token contains.

Equations

• s.view = Lean.TSyntax.getVersoRefName s

def Lean.Doc.VersoLinkUrl.view (s : VersoLinkUrl) : String

Decodes the URL that a Verso link or image token contains, interpreting escape sequences.

Equations

• s.view = Lean.TSyntax.getVersoLinkUrl s

def Lean.Doc.VersoLinkRefUrl.view (s : VersoLinkRefUrl) : String

Returns the URL that a Verso link reference definition token contains. These positions do not support escape sequences.

Equations

• s.view = Lean.TSyntax.getVersoLinkRefUrl s

def Lean.Doc.VersoImageAlt.view (s : VersoImageAlt) : String

Decodes the alternate text that a Verso image token contains, interpreting escape sequences.

Equations

• s.view = Lean.TSyntax.getVersoImageAlt s

def Lean.Doc.VersoCodeLine.view (s : VersoCodeLine) : String

Returns the text of one source line inside Verso inline code or a Verso code block.

Equations

• s.view = Lean.TSyntax.getVersoCodeLine s

def Lean.Doc.VersoCode.view (s : VersoCode) : String

Returns the code that Verso inline code content denotes, which is the text of its lines in order.

Equations

• s.view = Lean.TSyntax.getVersoCode s

def Lean.Doc.VersoCodeBlock.view (s : VersoCodeBlock) : String

Returns the contents of a Verso code block, which are the texts of its lines in order.

Equations

• s.view = Lean.TSyntax.getVersoCodeBlock s

The kinds of the nodes that the Verso parser builds, grouped by syntax category as Lean.Parser.Term and Lean.Parser.Command are. The tokens that store literal content are declared above, with the accessors that decode them.

def Lean.Doc.Parser.ArgVal.str : Parser.Parser

Equations

• Lean.Doc.Parser.ArgVal.str = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "ArgVal.str" `Lean.Doc.Parser.ArgVal.str Lean.Parser.strLit

def Lean.Doc.Parser.ArgVal.ident : Parser.Parser

Equations

• Lean.Doc.Parser.ArgVal.ident = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "ArgVal.ident" `Lean.Doc.Parser.ArgVal.ident Lean.Parser.ident

def Lean.Doc.Parser.ArgVal.num : Parser.Parser

Equations

• Lean.Doc.Parser.ArgVal.num = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "ArgVal.num" `Lean.Doc.Parser.ArgVal.num Lean.Parser.numLit

def Lean.Doc.Parser.argVal : Parser.Parser

Argument values. Quotations may use antiquotations for any of the forms.

Equations

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

def Lean.Doc.Parser.Arg.anon : Parser.Parser

Anonymous positional argument

Equations

• Lean.Doc.Parser.Arg.anon = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "anon" `Lean.Doc.Parser.Arg.anon Lean.Doc.Parser.argVal

def Lean.Doc.Parser.Arg.named : Parser.Parser

Named argument

Equations

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

def Lean.Doc.Parser.Arg.named_no_paren : Parser.Parser

Named argument

Equations

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

def Lean.Doc.Parser.Arg.flag_on : Parser.Parser

Boolean flag, turned on

Equations

• Lean.Doc.Parser.Arg.flag_on = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "flag_on" `Lean.Doc.Parser.Arg.flag_on (Lean.Parser.symbol "+" >> Lean.Parser.ident)

def Lean.Doc.Parser.Arg.flag_off : Parser.Parser

Boolean flag, turned off

Equations

• Lean.Doc.Parser.Arg.flag_off = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "flag_off" `Lean.Doc.Parser.Arg.flag_off (Lean.Parser.symbol "-" >> Lean.Parser.ident)

def Lean.Doc.Parser.arg : Parser.Parser

Arguments to a role, directive, command, or code block.

Equations

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

def Lean.Doc.Parser.LinkTarget.url : Parser.Parser

A URL target, written explicitly. Use square brackets for a named target.

Equations

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

def Lean.Doc.Parser.LinkTarget.ref : Parser.Parser

A named reference to a URL defined elsewhere. Use parentheses to write the URL here.

Equations

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

def Lean.Doc.Parser.linkTarget : Parser.Parser

The target of a link or image.

Equations

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

def Lean.Doc.Parser.headerMarker : Parser.Parser

The sequence of # characters that introduces a header. Its length determines the header's level.

Equations

• Lean.Doc.Parser.headerMarker = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "headerMarker" `Lean.Doc.Parser.headerMarker (Lean.Doc.Parser.charRun✝ '#')

def Lean.Doc.Parser.listMarker : Parser.Parser

The marker that introduces a list item. An unordered list uses *, -, or +. An ordered list uses a number followed by . or ).

Equations

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

def Lean.Doc.Parser.emphDelimiter : Parser.Parser

The run of _ characters that delimits emphasis.

Equations

• Lean.Doc.Parser.emphDelimiter = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "emphDelimiter" `Lean.Doc.Parser.emphDelimiter (Lean.Doc.Parser.charRun✝ '_')

def Lean.Doc.Parser.boldDelimiter : Parser.Parser

The sequence of * characters that delimits bold text.

Equations

• Lean.Doc.Parser.boldDelimiter = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "boldDelimiter" `Lean.Doc.Parser.boldDelimiter (Lean.Doc.Parser.charRun✝ '*')

def Lean.Doc.Parser.codeDelimiter : Parser.Parser

The sequence of backticks that delimits inline code. Longer delimiters allow backticks in the content.

Equations

• Lean.Doc.Parser.codeDelimiter = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "codeDelimiter" `Lean.Doc.Parser.codeDelimiter (Lean.Doc.Parser.charRun✝ '`')

def Lean.Doc.Parser.codeBlockFence : Parser.Parser

The fence that surrounds a code block. Longer fences allow more backticks in the content.

Equations

• Lean.Doc.Parser.codeBlockFence = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "codeBlockFence" `Lean.Doc.Parser.codeBlockFence (Lean.Doc.Parser.charRun✝ '`')

def Lean.Doc.Parser.inlineMathMarker : Parser.Parser

The $ that introduces inline mathematical notation. $ begins an antiquotation, so a quotation splices this atom in as $m:inlineMathMarker.

Equations

• Lean.Doc.Parser.inlineMathMarker = Lean.Doc.Parser.onFirstUse✝ fun (x : Unit) => Lean.Parser.nodeWithAntiquot "inlineMathMarker" `Lean.Doc.Parser.inlineMathMarker (Lean.Doc.Parser.atomOf✝ "$")

def Lean.Doc.Parser.displayMathMarker : Parser.Parser

The $ that introduces inline mathematical notation. $ begins an antiquotation, so a quotation splices this atom in as $m:inlineMathMarker.

Equations

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

def Lean.Doc.Parser.directiveDelimiter : Parser.Parser

The sequence of : characters that delimits a directive.

Equations

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

def Lean.Doc.Parser.Inline.text : Parser.Parser

Equations

• Lean.Doc.Parser.Inline.text = { fn := Lean.Doc.Parser.textQuot✝ }

def Lean.Doc.Parser.Inline.emph : Parser.Parser

Emphasis, often rendered as italics.

Emphasis may be nested by using longer sequences of _ for the outer delimiters.

Equations

• Lean.Doc.Parser.Inline.emph = { fn := Lean.Doc.Parser.emphQuot✝ }

def Lean.Doc.Parser.Inline.bold : Parser.Parser

Bold emphasis.

A single * suffices to make text bold. Use _ for emphasis.

Bold text may be nested by using longer sequences of * for the outer delimiters.

Equations

• Lean.Doc.Parser.Inline.bold = { fn := Lean.Doc.Parser.boldQuot✝ }

def Lean.Doc.Parser.Inline.code : Parser.Parser

Literal code.

Code may begin with any non-zero number of backticks. It must be terminated with the same number, and it may not contain a sequence of backticks that is at least as long as its starting or ending delimiters.

If the first and last characters are space, and it contains at least one non-space character, then the resulting string has a single space stripped from each end. Thus, `` `x `` represents "`x", not " `x ".

Equations

• Lean.Doc.Parser.Inline.code = Lean.Doc.Parser.inlineCode✝

def Lean.Doc.Parser.Inline.inline_math : Parser.Parser

Inline mathematical notation (equivalent to LaTeX's $ notation)

Equations

• Lean.Doc.Parser.Inline.inline_math = { fn := Lean.Doc.Parser.inlineMathQuot✝ }

def Lean.Doc.Parser.Inline.display_math : Parser.Parser

Display-mode mathematical notation

Equations

• Lean.Doc.Parser.Inline.display_math = { fn := Lean.Doc.Parser.displayMathQuot✝ }

def Lean.Doc.Parser.Inline.link : Parser.Parser

A link. The link's target may either be a concrete URL (written in parentheses) or a named URL (written in square brackets).

Equations

• Lean.Doc.Parser.Inline.link = { fn := Lean.Doc.Parser.linkQuot✝ }

def Lean.Doc.Parser.Inline.image : Parser.Parser

An image, with alternate text and a URL.

The alternate text is a plain string, rather than Verso markup.

The image URL may either be a concrete URL (written in parentheses) or a named URL (written in square brackets).

Equations

• Lean.Doc.Parser.Inline.image = { fn := Lean.Doc.Parser.imageQuot✝ }

def Lean.Doc.Parser.Inline.footnote : Parser.Parser

A footnote use site.

Footnotes must be defined elsewhere using the [^NAME]: TEXT syntax.

Equations

• Lean.Doc.Parser.Inline.footnote = { fn := Lean.Doc.Parser.footnoteQuot✝ }

def Lean.Doc.Parser.Inline.linebreak : Parser.Parser

Equations

• Lean.Doc.Parser.Inline.linebreak = { fn := Lean.Doc.Parser.linebreakQuot✝ }

def Lean.Doc.Parser.Inline.role : Parser.Parser

A role is an extension to the Verso document language in an inline position.

Text is given a role using the following syntax: {NAME ARGS*}[CONTENT]. The NAME is an identifier that determines which role is being used, akin to a function name. Each of the ARGS may have the following forms:

• A value, which is a string literal, natural number, or identifier
• A named argument, of the form (NAME := VALUE)
• A flag, of the form +NAME or -NAME

The CONTENT is a sequence of inline content. If there is only one piece of content and it has beginning and ending delimiters (e.g. code literals, links, or images, but not ordinary text), then the [ and ] may be omitted. In particular, {NAME ARGS*}`x` is equivalent to {NAME ARGS*}[`x`].

Equations

• Lean.Doc.Parser.Inline.role = { fn := Lean.Doc.Parser.roleQuot✝ }

def Lean.Doc.Parser.inline : Parser.Parser

Any inline element.

Equations

• Lean.Doc.Parser.inline = { fn := Lean.Doc.Parser.inlineQuot✝ }

def Lean.Doc.Parser.ListItem.item : Parser.Parser

A list item

Equations

• Lean.Doc.Parser.ListItem.item = { fn := Lean.Doc.Parser.listItemQuot✝ Lean.Doc.Parser.listMarker }

def Lean.Doc.Parser.DescItem.item : Parser.Parser

A description of an item

Equations

• Lean.Doc.Parser.DescItem.item = { fn := Lean.Doc.Parser.descItemQuot✝ }

def Lean.Doc.Parser.Block.para : Parser.Parser

Paragraph

Equations

• Lean.Doc.Parser.Block.para = { fn := Lean.Doc.Parser.paraQuot✝ }

def Lean.Doc.Parser.Block.ul : Parser.Parser

Unordered List

Equations

• Lean.Doc.Parser.Block.ul = { fn := Lean.Doc.Parser.ulQuot✝ }

def Lean.Doc.Parser.Block.ol : Parser.Parser

Ordered list

Equations

• Lean.Doc.Parser.Block.ol = { fn := Lean.Doc.Parser.olQuot✝ }

def Lean.Doc.Parser.Block.dl : Parser.Parser

Description list

Equations

• Lean.Doc.Parser.Block.dl = { fn := Lean.Doc.Parser.dlQuot✝ }

def Lean.Doc.Parser.Block.blockquote : Parser.Parser

A quotation, which contains a sequence of blocks that are at least as indented as the >.

Equations

• Lean.Doc.Parser.Block.blockquote = { fn := Lean.Doc.Parser.blockquoteQuot✝ }

def Lean.Doc.Parser.Block.codeblock : Parser.Parser

A code block that contains literal code. The contents of a code block are not written in Verso syntax.

Code blocks have the following syntax:

```(NAME ARGS*)?
CONTENT
```

CONTENT is a literal string. If the CONTENT contains a sequence of three or more backticks, then the opening and closing ``` (called fences) must have more backticks than the longest sequence in CONTENT. Additionally, the opening and closing fences must have the same number of backticks.

If NAME and ARGS are not provided, then the code block represents literal text. If provided, the NAME is an identifier that selects an interpretation of the block. Unlike Markdown, this name is not necessarily the language in which the code is written, though many custom code blocks are, in practice, named after the language that they contain. NAME is more akin to a function name that determines the interpretation of the code block's contents. Each of the ARGS may have the following forms:

• A value, which is a string literal, natural number, or identifier
• A named argument, of the form (NAME := VALUE)
• A flag, of the form +NAME or -NAME

The CONTENT is interpreted according to the indentation of the fences. If the fences are indented n spaces, then n spaces are removed from the start of each line of CONTENT.

Equations

• Lean.Doc.Parser.Block.codeblock = { fn := Lean.Doc.Parser.codeblockQuot✝ }

def Lean.Doc.Parser.Block.directive : Parser.Parser

A directive, which is an extension to the Verso language in block position. The contents of a directive are written in Verso syntax.

Directives have the following syntax:

:::NAME ARGS*
CONTENT*
:::

The NAME is an identifier that determines which directive is being used, akin to a function name. Each of the ARGS may have the following forms:

• A value, which is a string literal, natural number, or identifier
• A named argument, of the form (NAME := VALUE)
• A flag, of the form +NAME or -NAME

The CONTENT is a sequence of block content. Directives may be nested by using more colons in the outer directive. For example:

::::outer +flag (arg := 5)
A paragraph.
:::inner "label"
* 1
* 2
:::
::::

Equations

• Lean.Doc.Parser.Block.directive = { fn := Lean.Doc.Parser.directiveQuot✝ }

def Lean.Doc.Parser.Block.header : Parser.Parser

A header

Headers must be correctly nested to form a tree structure. The first header in a document must start with #, and subsequent headers must have at most one more # than the preceding header.

Equations

• Lean.Doc.Parser.Block.header = { fn := Lean.Doc.Parser.headerQuot✝ }

def Lean.Doc.Parser.Block.link_ref : Parser.Parser

A named URL that can be used in links and images.

Equations

• Lean.Doc.Parser.Block.link_ref = { fn := Lean.Doc.Parser.linkRefQuot✝ }

def Lean.Doc.Parser.Block.footnote_ref : Parser.Parser

A footnote definition.

Equations

• Lean.Doc.Parser.Block.footnote_ref = { fn := Lean.Doc.Parser.footnoteRefQuot✝ }

def Lean.Doc.Parser.Block.metadata_block : Parser.Parser

Metadata for the preceding header.

Equations

• Lean.Doc.Parser.Block.metadata_block = { fn := Lean.Doc.Parser.metadataQuot✝ }

def Lean.Doc.Parser.Block.command : Parser.Parser

A block-level command, which invokes an extension during documentation processing.

The NAME is an identifier that determines which command is being used, akin to a function name. Each of the ARGS may have the following forms:

• A value, which is a string literal, natural number, or identifier
• A named argument, of the form (NAME := VALUE)
• A flag, of the form +NAME or -NAME

Equations

• Lean.Doc.Parser.Block.command = { fn := Lean.Doc.Parser.commandQuot✝ }

def Lean.Doc.Parser.block : Parser.Parser

Any block element.

Equations

• Lean.Doc.Parser.block = { fn := Lean.Doc.Parser.blockQuot✝ }

def Lean.Doc.Parser.document : Parser.Parser

A Verso document, which is a sequence of blocks.

Equations

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

@[reducible, inline]

abbrev Lean.Doc.VersoInline : Type

An inline element of a Verso document, such as text, emphasis, or a link.

Use VersoInline.view to inspect it.

Equations

• Lean.Doc.VersoInline = Lean.TSyntax `Lean.Doc.Parser.inline

@[reducible, inline]

abbrev Lean.Doc.VersoBlock : Type

A block-level element of a Verso document, such as a paragraph, a list, or a code block.

Use VersoBlock.view to inspect it.

Equations

• Lean.Doc.VersoBlock = Lean.TSyntax `Lean.Doc.Parser.block

@[reducible, inline]

abbrev Lean.Doc.VersoDelimiter : Type

A delimiter of a Verso element, such as the backticks around a code literal or the asterisks around bold text. The markers that introduce a header, a list item, and mathematical notation are delimiters too.

Each sits in a node of its own, so that a quotation can splice one in place of writing it out. Use VersoDelimiter.view or TSyntax.getVersoDelimiter to read its characters.

Equations

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

def Lean.TSyntax.getVersoBlocks (doc : Doc.VersoDocument) : TSyntaxArray `Lean.Doc.Parser.block

Extracts the blocks of a Verso document.

Equations

• Lean.TSyntax.getVersoBlocks doc = Array.map (fun (x : Lean.Syntax) => { raw := x }) doc.raw[0].getArgs

def Lean.TSyntax.getVersoDelimiter (delim : Doc.VersoDelimiter) : String

Returns the characters that make up a Verso delimiter.

Equations

• Lean.TSyntax.getVersoDelimiter delim = delim.raw[0].getAtomVal

def Lean.Doc.VersoDocument.view (doc : VersoDocument) : Array VersoBlock

Extracts the blocks of a Verso document.

Equations

• doc.view = Lean.TSyntax.getVersoBlocks doc

def Lean.Doc.VersoDelimiter.view (delim : VersoDelimiter) : String

Returns the characters that make up a Verso delimiter.

Equations

• delim.view = Lean.TSyntax.getVersoDelimiter delim

@[instance_reducible]

instance Lean.Doc.instCoeVersoDocumentTSyntaxArrayConsSyntaxNodeKindMkStr4Nil : Coe VersoDocument (TSyntaxArray `Lean.Doc.Parser.block)

A document stands for the blocks it contains.

Equations

• Lean.Doc.instCoeVersoDocumentTSyntaxArrayConsSyntaxNodeKindMkStr4Nil = { coe := fun (doc : Lean.Doc.VersoDocument) => Lean.TSyntax.getVersoBlocks doc }

Each inline and block element can be used where its category is expected, so an element with a known kind can be spliced into a quotation.

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean : Coe (TSyntax `Lean.Doc.Parser.Inline.text) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.text) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_1 : Coe (TSyntax `Lean.Doc.Parser.Inline.emph) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_1 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.emph) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_2 : Coe (TSyntax `Lean.Doc.Parser.Inline.bold) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_2 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.bold) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_3 : Coe (TSyntax `Lean.Doc.Parser.Inline.code) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_3 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.code) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_4 : Coe (TSyntax `Lean.Doc.Parser.Inline.inline_math) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_4 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.inline_math) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_5 : Coe (TSyntax `Lean.Doc.Parser.Inline.display_math) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_5 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.display_math) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_6 : Coe (TSyntax `Lean.Doc.Parser.Inline.link) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_6 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.link) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_7 : Coe (TSyntax `Lean.Doc.Parser.Inline.image) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_7 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.image) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_8 : Coe (TSyntax `Lean.Doc.Parser.Inline.footnote) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_8 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.footnote) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_9 : Coe (TSyntax `Lean.Doc.Parser.Inline.linebreak) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_9 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.linebreak) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_10 : Coe (TSyntax `Lean.Doc.Parser.Inline.role) (TSyntax `Lean.Doc.Parser.inline)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_10 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Inline.role) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_11 : Coe (TSyntax `Lean.Doc.Parser.Block.para) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_11 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.para) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_12 : Coe (TSyntax `Lean.Doc.Parser.Block.ul) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_12 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.ul) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_13 : Coe (TSyntax `Lean.Doc.Parser.Block.ol) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_13 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.ol) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_14 : Coe (TSyntax `Lean.Doc.Parser.Block.dl) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_14 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.dl) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_15 : Coe (TSyntax `Lean.Doc.Parser.Block.blockquote) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_15 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.blockquote) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_16 : Coe (TSyntax `Lean.Doc.Parser.Block.codeblock) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_16 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.codeblock) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_17 : Coe (TSyntax `Lean.Doc.Parser.Block.directive) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_17 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.directive) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_18 : Coe (TSyntax `Lean.Doc.Parser.Block.header) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_18 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.header) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_19 : Coe (TSyntax `Lean.Doc.Parser.Block.link_ref) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_19 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.link_ref) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_20 : Coe (TSyntax `Lean.Doc.Parser.Block.footnote_ref) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_20 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.footnote_ref) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_21 : Coe (TSyntax `Lean.Doc.Parser.Block.metadata_block) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_21 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.metadata_block) => { raw := s.raw } }

@[instance_reducible]

instance Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_22 : Coe (TSyntax `Lean.Doc.Parser.Block.command) (TSyntax `Lean.Doc.Parser.block)

Equations

• Lean.Doc.instCoeTSyntaxConsSyntaxNodeKindMkStr5NilMkStr4_lean_22 = { coe := fun (s : Lean.TSyntax `Lean.Doc.Parser.Block.command) => { raw := s.raw } }