This module contains an internal syntax that's used to represent documents.

Ordinarily, a syntax declaration is used to extend the Lean parser. The parser produces Syntax, which is flexible enough to represent essentially anything. However, each syntax declaration will produce parsed syntax trees with a predictable form, and these syntax trees can be matched using quasiquotation patterns. In other words, syntax declarations really do all of the following:

• They extend Lean's parser
• They establish expectations for valid subsets of Syntax
• They provide a way to pattern-match against the valid Syntax that they induce

The syntax declarations in this module are used somewhat differently. They're not generally intended for direct use with the Lean parser, because the concrete syntax of Verso documents falls outside what can be implemented with Lean's parsing framework. Thus, Verso has a separate parser, written using the lower-level parts of Lean's parser. These syntax declarations are, however, a specification for the syntax trees produced by said parser. The Verso parser is in the module Lean.DocString.Parser. Specifying the Verso document syntax as is done here also allows quasiquotation patterns that match against the output of the Verso parser.

Importantly, Lean quasiquotation patterns do not match the string contents of atoms. This means that the Verso parser may produce a node of kind `Lean.Doc.Syntax.li in which the first atom is "1." rather than "*' when parsing an ordered list.

Parsed Verso documents are transformed into Lean syntax that represents Verso document ASTs (see module Lean.DocString.Types). This process potentially invokes user-written metaprograms - while Verso's concrete syntax is not extensible, roles, directives and code blocks all contain explicit hooks for extensibility. This translation step is defined in the module Lean.DocString.Elab.

def Lean.Doc.Syntax.arg_val.quot : ParserDescr

Equations

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

def Lean.Parser.Category.arg_val : Category

Argument values

Equations

• Lean.Parser.Category.arg_val = { }

def Lean.Doc.Syntax.arg_str : ParserDescr

Equations

• Lean.Doc.Syntax.arg_str = Lean.ParserDescr.node `Lean.Doc.Syntax.arg_str 1022 (Lean.ParserDescr.const `str)

def Lean.Doc.Syntax.arg_ident : ParserDescr

Equations

• Lean.Doc.Syntax.arg_ident = Lean.ParserDescr.node `Lean.Doc.Syntax.arg_ident 1022 (Lean.ParserDescr.const `ident)

def Lean.Doc.Syntax.arg_num : ParserDescr

Equations

• Lean.Doc.Syntax.arg_num = Lean.ParserDescr.node `Lean.Doc.Syntax.arg_num 1022 (Lean.ParserDescr.const `num)

def Lean.Doc.Syntax.doc_arg.quot : ParserDescr

Equations

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

def Lean.Parser.Category.doc_arg : Category

Arguments

Equations

• Lean.Parser.Category.doc_arg = { }

def Lean.Doc.Syntax.anon : ParserDescr

Anonymous positional arguments

Equations

• Lean.Doc.Syntax.anon = Lean.ParserDescr.node `Lean.Doc.Syntax.anon 1022 (Lean.ParserDescr.cat `arg_val 0)

def Lean.Doc.Syntax.named : ParserDescr

Named arguments

Equations

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

def Lean.Doc.Syntax.named_no_paren : ParserDescr

Named arguments, without parentheses.

Equations

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

def Lean.Doc.Syntax.flag_on : ParserDescr

Boolean flags, turned on

Equations

• Lean.Doc.Syntax.flag_on = Lean.ParserDescr.node `Lean.Doc.Syntax.flag_on 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+") (Lean.ParserDescr.const `ident))

def Lean.Doc.Syntax.flag_off : ParserDescr

Boolean flags, turned off

Equations

• Lean.Doc.Syntax.flag_off = Lean.ParserDescr.node `Lean.Doc.Syntax.flag_off 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "-") (Lean.ParserDescr.const `ident))

def Lean.Doc.Syntax.link_target.quot : ParserDescr

Equations

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

def Lean.Parser.Category.link_target : Category

Link targets, which may be URLs or named references

Equations

• Lean.Parser.Category.link_target = { }

def Lean.Doc.Syntax.url : ParserDescr

A reference to a URL

Equations

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

def Lean.Doc.Syntax.ref : ParserDescr

A named reference

Equations

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

def Lean.Parser.Category.inline : Category

Verso inline objects. These are part of the ordinary text flow of a paragraph.

This syntax uses the following conventions:

• Sequences of inline items are in square brackets
• Literal data, like strings or numbers, are in parentheses
• Verso metaprogram names and arguments are in curly braces

Equations

• Lean.Parser.Category.inline = { }

def Lean.Doc.Syntax.inline.quot : ParserDescr

Equations

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

def Lean.Doc.Syntax.text : ParserDescr

Equations

• Lean.Doc.Syntax.text = Lean.ParserDescr.node `Lean.Doc.Syntax.text 1022 (Lean.ParserDescr.const `str)

def Lean.Doc.Syntax.emph : ParserDescr

Emphasis (often rendered as italics)

Equations

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

def Lean.Doc.Syntax.bold : ParserDescr

Bold emphasis

Equations

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

def Lean.Doc.Syntax.link : ParserDescr

Link

Equations

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

def Lean.Doc.Syntax.image : ParserDescr

Image

Equations

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

def Lean.Doc.Syntax.footnote : ParserDescr

A footnote use

Equations

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

def Lean.Doc.Syntax.linebreak : ParserDescr

Line break

Equations

• Lean.Doc.Syntax.linebreak = Lean.ParserDescr.node `Lean.Doc.Syntax.linebreak 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "line!") (Lean.ParserDescr.const `str))

def Lean.Doc.Syntax.code : ParserDescr

Literal code. 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.

Equations

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

def Lean.Doc.Syntax.role : ParserDescr

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

Equations

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

def Lean.Doc.Syntax.inline_math : ParserDescr

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

Equations

• Lean.Doc.Syntax.inline_math = Lean.ParserDescr.node `Lean.Doc.Syntax.inline_math 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "\\math") Lean.Doc.Syntax.code)

def Lean.Doc.Syntax.display_math : ParserDescr

Display-mode mathematical notation

Equations

• Lean.Doc.Syntax.display_math = Lean.ParserDescr.node `Lean.Doc.Syntax.display_math 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "\\displaymath") Lean.Doc.Syntax.code)

def Lean.Parser.Category.block : Category

Block-level elements, such as paragraphs, headers, and lists.

Conventions:

• When there's concrete syntax that can be written as Lean atoms, do so (code blocks are ```, directives :::)
• When Verso's syntax requires a newline, use | because "\n" is not a valid Lean token
• Directive bodies are in { and } to avoid quotation parsing issues with ::: ... :::
• If there's no concrete syntax per se, such as for paragraphs or lists, use a name with brackets and braces
• Use parentheses around required literals, such as the starting number of an ordered list
• Use square brackets around sequences of literals
• Use curly braces around blocks or lists items (because names and arguments a la roles are always newline-separated for directives and code)

Equations

• Lean.Parser.Category.block = { }

def Lean.Doc.Syntax.block.quot : ParserDescr

Equations

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

def Lean.Parser.Category.list_item : Category

Items from both ordered and unordered lists

Equations

• Lean.Parser.Category.list_item = { }

def Lean.Doc.Syntax.list_item.quot : ParserDescr

Equations

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

def Lean.Doc.Syntax.li : ParserDescr

List item

Equations

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

def Lean.Parser.Category.desc_item : Category

A description of an item

Equations

• Lean.Parser.Category.desc_item = { }

def Lean.Doc.Syntax.desc_item.quot : ParserDescr

Equations

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

def Lean.Doc.Syntax.desc : ParserDescr

A description of an item

Equations

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

def Lean.Doc.Syntax.para : ParserDescr

Equations

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

def Lean.Doc.Syntax.ul : ParserDescr

Unordered List

Equations

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

def Lean.Doc.Syntax.dl : ParserDescr

Definition list

Equations

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

def Lean.Doc.Syntax.ol : ParserDescr

Ordered list

Equations

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

def Lean.Doc.Syntax.codeblock : ParserDescr

Literal code

Equations

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

def Lean.Doc.Syntax.blockquote : ParserDescr

Quotation

Equations

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

def Lean.Doc.Syntax.link_ref : ParserDescr

A link reference definition

Equations

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

def Lean.Doc.Syntax.footnote_ref : ParserDescr

A footnote definition

Equations

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

def Lean.Doc.Syntax.directive : ParserDescr

Custom directive

Equations

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

def Lean.Doc.Syntax.header : ParserDescr

A header

Equations

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

def Lean.Doc.Syntax.metadataContents : Parser.Parser

Equations

• Lean.Doc.Syntax.metadataContents = Lean.Parser.Term.structInstFields (Lean.Parser.sepByIndent Lean.Parser.Term.structInstField ", " (Lean.Parser.symbol ", ") true)

def Lean.Doc.Syntax.metadata_block : ParserDescr

Metadata for this section, defined by the current genre

Equations

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

def Lean.Doc.Syntax.command : ParserDescr

A block-level command

Equations

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