This module defines views of the concrete syntax of Verso documents.

The syntax declarations in Lean.DocString.Syntax specify the shapes of the trees that the Verso parser and quotations produce. Views expose one level of this structure at a time as ordinary Lean datatypes. Each view node records the syntax it represents, the delimiter atoms that tooling such as semantic highlighting needs, and decoded values for literal content. Using views allows clients to avoid needing to check for things like optional brackets at all sites.

An of function returns none when the syntax does not have the specified shape. The parser and quotations produce only well-formed trees, so a none result indicates a bug. Callers report it as an error at the syntax in question.

inductive Lean.Doc.ArgValView : Type

A view of the value of an argument to a role, directive, command, or code block.

• str (lit : StrLit) (value : String) : ArgValView

  A string literal. value is its decoded contents.

• name (x : Ident) : ArgValView

  An identifier.

• num (lit : NumLit) (value : Nat) : ArgValView

  A numeric literal. value is its decoded value.

def Lean.Doc.ArgValView.of (stx : TSyntax `Lean.Doc.Parser.argVal) : Option ArgValView

A view of stx, if it is an argument value.

Equations

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

inductive Lean.Doc.ArgView : Type

A view of an argument to a role, directive, command, or code block.

• anon (stx : TSyntax `Lean.Doc.Parser.arg) (val : TSyntax `Lean.Doc.Parser.argVal) : ArgView

  An anonymous positional argument.

• named (stx : TSyntax `Lean.Doc.Parser.arg) (parens : Option (Syntax × Syntax)) (name : Ident) (assign : Syntax) (val : TSyntax `Lean.Doc.Parser.argVal) : ArgView

  A named argument. parens is the pair of parenthesis atoms when the argument is written in parentheses, and assign is the := atom.

• flag (stx : TSyntax `Lean.Doc.Parser.arg) (sign : Syntax) (name : Ident) (isOn : Bool) : ArgView

  A flag. sign is the + or - atom, and isOn indicates which one it is.

def Lean.Doc.ArgView.stx : ArgView → TSyntax `Lean.Doc.Parser.arg

Returns the syntax underlying an argument view.

Equations

• (Lean.Doc.ArgView.anon stx val).stx = stx
• (Lean.Doc.ArgView.named stx parens name assign val).stx = stx
• (Lean.Doc.ArgView.flag stx sign name isOn).stx = stx

def Lean.Doc.ArgView.of (stx : TSyntax `Lean.Doc.Parser.arg) : Option ArgView

A view of stx, if it is an argument.

Equations

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

inductive Lean.Doc.LinkTargetView : Type

A view of a link target, which is either a URL or a reference to a URL defined elsewhere.

• url (stx : TSyntax `Lean.Doc.Parser.linkTarget) (opener : Syntax) (url : VersoLinkUrl) (closer : Syntax) : LinkTargetView

  A URL written directly, in parentheses. Use TSyntax.getVersoLinkUrl to read it.

• ref (stx : TSyntax `Lean.Doc.Parser.linkTarget) (opener : Syntax) (name : VersoRefName) (closer : Syntax) : LinkTargetView

  A reference to a URL defined elsewhere, in square brackets. Use TSyntax.getVersoRefName to read the name.

def Lean.Doc.mkVersoTextFrom (src : Syntax) (value : String) (canonical : Bool := false) : VersoText

Builds a text content token containing value, with its position taken from src.

Equations

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

def Lean.Doc.mkVersoRefNameFrom (src : Syntax) (value : String) (canonical : Bool := false) : VersoRefName

Builds the name of a footnote or link reference containing value, with its position taken from src.

Equations

• Lean.Doc.mkVersoRefNameFrom src value canonical = { raw := (Lean.Syntax.mkLit Lean.Doc.versoRefKind value (Lean.SourceInfo.fromRef src canonical)).raw }

def Lean.Doc.mkVersoLinkUrlFrom (src : Syntax) (value : String) (canonical : Bool := false) : VersoLinkUrl

Builds a link URL token containing value, with its position taken from src.

Equations

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

def Lean.Doc.mkVersoImageAltFrom (src : Syntax) (value : String) (canonical : Bool := false) : VersoImageAlt

Builds an image's alternate text containing value, with its position taken from src.

Equations

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

def Lean.Doc.mkVersoLinkRefUrlFrom (src : Syntax) (value : String) (canonical : Bool := false) : VersoLinkRefUrl

Builds the URL of a link reference definition containing value, with its position taken from src.

Equations

• Lean.Doc.mkVersoLinkRefUrlFrom src value canonical = { raw := (Lean.Syntax.mkLit Lean.Doc.versoLinkRefUrlKind value (Lean.SourceInfo.fromRef src canonical)).raw }

def Lean.Doc.mkVersoCodeFrom (src : Syntax) (value : String) (canonical : Bool := false) : VersoCode

Builds inline code content containing value, with one line token per line and its position taken from src.

Equations

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

def Lean.Doc.mkVersoCodeBlockFrom (src : Syntax) (value : String) (canonical : Bool := false) : VersoCodeBlock

Builds a code block's content containing value, with one line token per line and its position taken from src.

Equations

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

def Lean.Doc.mkVersoLinebreakFrom (src : Syntax) (canonical : Bool := false) : TSyntax `Lean.Doc.Parser.Inline.linebreak

Builds a line break, with its position taken from src.

Equations

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

def Lean.Doc.mkVersoLinebreakFromRef {m : Type → Type} [Monad m] [MonadRef m] (canonical : Bool := false) : m (TSyntax `Lean.Doc.Parser.Inline.linebreak)

Builds a line break, positioned at the current reference.

Equations

• Lean.Doc.mkVersoLinebreakFromRef canonical = do let __do_lift ← Lean.getRef pure (Lean.Doc.mkVersoLinebreakFrom __do_lift canonical)

def Lean.Doc.mkVersoTextFromRef {m : Type → Type} [Monad m] [MonadRef m] (value : String) (canonical : Bool := false) : m VersoText

Builds a text content token containing value, positioned at the current reference.

Equations

• Lean.Doc.mkVersoTextFromRef value canonical = do let __do_lift ← Lean.getRef pure (Lean.Doc.mkVersoTextFrom __do_lift value canonical)

def Lean.Doc.mkVersoRefNameFromRef {m : Type → Type} [Monad m] [MonadRef m] (value : String) (canonical : Bool := false) : m VersoRefName

Builds a reference name containing value, positioned at the current reference.

Equations

• Lean.Doc.mkVersoRefNameFromRef value canonical = do let __do_lift ← Lean.getRef pure (Lean.Doc.mkVersoRefNameFrom __do_lift value canonical)

def Lean.Doc.mkVersoLinkUrlFromRef {m : Type → Type} [Monad m] [MonadRef m] (value : String) (canonical : Bool := false) : m VersoLinkUrl

Builds a link URL containing value, positioned at the current reference.

Equations

• Lean.Doc.mkVersoLinkUrlFromRef value canonical = do let __do_lift ← Lean.getRef pure (Lean.Doc.mkVersoLinkUrlFrom __do_lift value canonical)

def Lean.Doc.mkVersoImageAltFromRef {m : Type → Type} [Monad m] [MonadRef m] (value : String) (canonical : Bool := false) : m VersoImageAlt

Builds an image's alternate text containing value, positioned at the current reference.

Equations

• Lean.Doc.mkVersoImageAltFromRef value canonical = do let __do_lift ← Lean.getRef pure (Lean.Doc.mkVersoImageAltFrom __do_lift value canonical)

def Lean.Doc.mkVersoLinkRefUrlFromRef {m : Type → Type} [Monad m] [MonadRef m] (value : String) (canonical : Bool := false) : m VersoLinkRefUrl

Builds the URL of a link reference definition containing value, positioned at the syntax getRef returns.

Equations

• Lean.Doc.mkVersoLinkRefUrlFromRef value canonical = do let __do_lift ← Lean.getRef pure (Lean.Doc.mkVersoLinkRefUrlFrom __do_lift value canonical)

def Lean.Doc.mkVersoCodeFromRef {m : Type → Type} [Monad m] [MonadRef m] (value : String) (canonical : Bool := false) : m VersoCode

Builds inline code content containing value, positioned at the current reference.

Equations

• Lean.Doc.mkVersoCodeFromRef value canonical = do let __do_lift ← Lean.getRef pure (Lean.Doc.mkVersoCodeFrom __do_lift value canonical)

def Lean.Doc.mkVersoCodeBlockFromRef {m : Type → Type} [Monad m] [MonadRef m] (value : String) (canonical : Bool := false) : m VersoCodeBlock

Builds a code block's content containing value, positioned at the current reference.

Equations

• Lean.Doc.mkVersoCodeBlockFromRef value canonical = do let __do_lift ← Lean.getRef pure (Lean.Doc.mkVersoCodeBlockFrom __do_lift value canonical)

def Lean.Doc.LinkTargetView.of (stx : TSyntax `Lean.Doc.Parser.linkTarget) : Option LinkTargetView

A view of stx, if it is a link target.

Equations

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

structure Lean.Doc.TextView : Type

A view of ordinary text.

• stx : TSyntax `Lean.Doc.Parser.inline

  The original syntax.

• content : VersoText

  The text.

@[instance_reducible]

instance Lean.Doc.instInhabitedTextView : Inhabited TextView

Equations

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

def Lean.Doc.TextView.getVersoText (v : TextView) : String

Decodes the Verso text contained in the view, interpreting escape sequences.

Equations

• v.getVersoText = Lean.TSyntax.getVersoText v.content

def Lean.Doc.TextView.getVersoTextSource (v : TextView) : String

Returns the literal representation of the text in the view, without interpreting escape sequences.

Equations

• v.getVersoTextSource = Lean.TSyntax.getVersoTextSource v.content

def Lean.Doc.TextView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option TextView

A view of stx, if it is ordinary text.

Equations

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

structure Lean.Doc.EmphView : Type

A view of emphasized content.

• stx : TSyntax `Lean.Doc.Parser.inline

  The original syntax.

• opener : TSyntax `Lean.Doc.Parser.emphDelimiter

  The opening run of _.

• content : TSyntaxArray `Lean.Doc.Parser.inline

  The emphasized content.

• closer : TSyntax `Lean.Doc.Parser.emphDelimiter

  The closing run of _.

def Lean.Doc.EmphView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option EmphView

A view of stx, if it is emphasized content.

Equations

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

structure Lean.Doc.BoldView : Type

A view of bold content.

• stx : TSyntax `Lean.Doc.Parser.inline

  The original syntax.

• opener : TSyntax `Lean.Doc.Parser.boldDelimiter

  The opening run of *.

• content : TSyntaxArray `Lean.Doc.Parser.inline

  The bold content.

• closer : TSyntax `Lean.Doc.Parser.boldDelimiter

  The closing run of *.

def Lean.Doc.BoldView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option BoldView

A view of stx, if it is bold content.

Equations

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

structure Lean.Doc.CodeView : Type

A view of literal code.

This view is used both for inline code elements and the body of math notation.

• stx : TSyntax `Lean.Doc.Parser.inline

  The original syntax.

• opener : TSyntax `Lean.Doc.Parser.codeDelimiter

  The opening run of backticks.

• content : VersoCode

  The code.

• closer : TSyntax `Lean.Doc.Parser.codeDelimiter

  The closing run of backticks.

def Lean.Doc.CodeView.getVersoCode (v : CodeView) : String

The decoded code contents

Equations

• v.getVersoCode = Lean.TSyntax.getVersoCode v.content

def Lean.Doc.CodeView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option CodeView

A view of stx, if it is inline code.

Equations

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

structure Lean.Doc.MathView : Type

A view of math content.

• stx : TSyntax `Lean.Doc.Parser.inline

  The original syntax.

• mode : MathMode

  Whether the mathematics should be typeset in inline or display mode.

• marker : TSyntax [`Lean.Doc.Parser.inlineMathMarker, `Lean.Doc.Parser.displayMathMarker]

  The $ or $$ marker.

• code : CodeView

  The LaTeX-style math code.

def Lean.Doc.MathView.getVersoCode (v : MathView) : String

The decoded code contents.

Equations

• v.getVersoCode = v.code.getVersoCode

def Lean.Doc.MathView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option MathView

A view of stx, if it is math content.

Math nests a code element, so the view contains the view of that element.

Equations

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

structure Lean.Doc.LinkView : Type

A view of a link.

• stx : TSyntax `Lean.Doc.Parser.inline

  The original syntax.

• opener : Syntax

  The [ that opens the link text.

• content : TSyntaxArray `Lean.Doc.Parser.inline

  The link text.

• closer : Syntax

  The ] that closes the link text.

• target : LinkTargetView

  Where the link leads.

def Lean.Doc.LinkView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option LinkView

A view of stx, if it is a link.

Equations

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

structure Lean.Doc.ImageView : Type

A view of an image.

• stx : TSyntax `Lean.Doc.Parser.inline

  The original syntax.

• opener : Syntax

  The ![ that opens the alternate text.

• alt : VersoImageAlt

  The alternate text.

• closer : Syntax

  The ] that closes the alternate text.

• target : LinkTargetView

  Where the image is found.

def Lean.Doc.ImageView.getAlt (v : ImageView) : String

The alternate text, with each escape replaced by the character it denotes.

Equations

• v.getAlt = Lean.TSyntax.getVersoImageAlt v.alt

def Lean.Doc.ImageView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option ImageView

A view of stx, if it is an image.

Equations

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

structure Lean.Doc.FootnoteView : Type

A view of a footnote use site.

• stx : TSyntax `Lean.Doc.Parser.inline

  The original syntax.

• opener : Syntax

  The [^ that opens the name.

• name : VersoRefName

  The name that refers to the footnote's definition.

• closer : Syntax

  The ] that closes the name.

def Lean.Doc.FootnoteView.getName (v : FootnoteView) : String

The name that refers to the footnote's definition.

Equations

• v.getName = Lean.TSyntax.getVersoRefName v.name

def Lean.Doc.FootnoteView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option FootnoteView

A view of stx, if it is a footnote use site.

Equations

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

structure Lean.Doc.LinebreakView : Type

A view of a line break.

• stx : TSyntax `Lean.Doc.Parser.inline

  The original syntax.

• newline : Syntax

  The newline atom.

def Lean.Doc.LinebreakView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option LinebreakView

A view of stx, if it is a line break.

Equations

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

structure Lean.Doc.RoleView : Type

A view of content with a role.

• stx : TSyntax `Lean.Doc.Parser.inline

  The original syntax.

• braceOpen : Syntax

  The { that opens the name and arguments.

• name : Ident

  The name that selects the role's expander.

• args : TSyntaxArray `Lean.Doc.Parser.arg

  The arguments to the role.

• braceClose : Syntax

  The } that closes the name and arguments.

• brackets : Option (Syntax × Syntax)

  The brackets around the content, if they are present.

• content : TSyntaxArray `Lean.Doc.Parser.inline

  The content that the role applies to.

def Lean.Doc.RoleView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option RoleView

A view of stx, if it is content with a role.

An author may write content that has delimiters of its own without brackets, so the brackets are matched separately from the name and arguments.

Equations

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

inductive Lean.Doc.InlineView : Type

A view of an inline document element.

• text (view : TextView) : InlineView

  Ordinary text.

• emph (view : EmphView) : InlineView

  Emphasized content.

• bold (view : BoldView) : InlineView

  Bold content.

• code (view : CodeView) : InlineView

  Literal code.

• math (view : MathView) : InlineView

  Mathematical notation.

• link (view : LinkView) : InlineView

  A link.

• image (view : ImageView) : InlineView

  An image.

• footnote (view : FootnoteView) : InlineView

  A footnote use site.

• linebreak (view : LinebreakView) : InlineView

  A soft line break.

• role (view : RoleView) : InlineView

  A role applied to some content.

@[instance_reducible]

instance Lean.Doc.instInhabitedInlineView : Inhabited InlineView

Equations

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

@[instance_reducible]

instance Lean.Doc.instCoeTextViewInlineView : Coe TextView InlineView

Equations

• Lean.Doc.instCoeTextViewInlineView = { coe := Lean.Doc.InlineView.text }

@[instance_reducible]

instance Lean.Doc.instCoeEmphViewInlineView : Coe EmphView InlineView

Equations

• Lean.Doc.instCoeEmphViewInlineView = { coe := Lean.Doc.InlineView.emph }

@[instance_reducible]

instance Lean.Doc.instCoeBoldViewInlineView : Coe BoldView InlineView

Equations

• Lean.Doc.instCoeBoldViewInlineView = { coe := Lean.Doc.InlineView.bold }

@[instance_reducible]

instance Lean.Doc.instCoeCodeViewInlineView : Coe CodeView InlineView

Equations

• Lean.Doc.instCoeCodeViewInlineView = { coe := Lean.Doc.InlineView.code }

@[instance_reducible]

instance Lean.Doc.instCoeMathViewInlineView : Coe MathView InlineView

Equations

• Lean.Doc.instCoeMathViewInlineView = { coe := Lean.Doc.InlineView.math }

@[instance_reducible]

instance Lean.Doc.instCoeLinkViewInlineView : Coe LinkView InlineView

Equations

• Lean.Doc.instCoeLinkViewInlineView = { coe := Lean.Doc.InlineView.link }

@[instance_reducible]

instance Lean.Doc.instCoeImageViewInlineView : Coe ImageView InlineView

Equations

• Lean.Doc.instCoeImageViewInlineView = { coe := Lean.Doc.InlineView.image }

@[instance_reducible]

instance Lean.Doc.instCoeFootnoteViewInlineView : Coe FootnoteView InlineView

Equations

• Lean.Doc.instCoeFootnoteViewInlineView = { coe := Lean.Doc.InlineView.footnote }

@[instance_reducible]

instance Lean.Doc.instCoeLinebreakViewInlineView : Coe LinebreakView InlineView

Equations

• Lean.Doc.instCoeLinebreakViewInlineView = { coe := Lean.Doc.InlineView.linebreak }

@[instance_reducible]

instance Lean.Doc.instCoeRoleViewInlineView : Coe RoleView InlineView

Equations

• Lean.Doc.instCoeRoleViewInlineView = { coe := Lean.Doc.InlineView.role }

def Lean.Doc.InlineView.stx : InlineView → TSyntax `Lean.Doc.Parser.inline

Returns the original syntax that an inline view was constructed from.

Equations

• (Lean.Doc.InlineView.text v).stx = v.stx
• (Lean.Doc.InlineView.emph v).stx = v.stx
• (Lean.Doc.InlineView.bold v).stx = v.stx
• (Lean.Doc.InlineView.code v).stx = v.stx
• (Lean.Doc.InlineView.math v).stx = v.stx
• (Lean.Doc.InlineView.link v).stx = v.stx
• (Lean.Doc.InlineView.image v).stx = v.stx
• (Lean.Doc.InlineView.footnote v).stx = v.stx
• (Lean.Doc.InlineView.linebreak v).stx = v.stx
• (Lean.Doc.InlineView.role v).stx = v.stx

def Lean.Doc.InlineView.of (stx : TSyntax `Lean.Doc.Parser.inline) : Option InlineView

A view of stx, if it is an inline document element.

Each production has a view of its own, and this tries them in turn. The productions have distinct syntax kinds, so at most one applies and the order does not matter.

Equations

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

structure Lean.Doc.UnorderedListItemView : Type

A view of an item of an unordered list.

• stx : TSyntax `Lean.Doc.Parser.ListItem.item

  The original syntax.

• marker : TSyntax `Lean.Doc.Parser.listMarker

  The marker, which is *, -, or +.

• contents : TSyntaxArray `Lean.Doc.Parser.block

  The item's contents.

def Lean.Doc.UnorderedListItemView.of (stx : TSyntax `Lean.Doc.Parser.ListItem.item) : Option UnorderedListItemView

A view of stx, if it is an unordered list's item. Its marker must be a bullet.

Equations

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

structure Lean.Doc.OrderedListItemView : Type

A view of an item of an ordered list.

• stx : TSyntax `Lean.Doc.Parser.ListItem.item

  The original syntax.

• marker : TSyntax `Lean.Doc.Parser.listMarker

  The marker, which is a number followed by . or ).

• contents : TSyntaxArray `Lean.Doc.Parser.block

  The item's contents.

def Lean.Doc.OrderedListItemView.number (v : OrderedListItemView) : Option Nat

The number that the item's marker gives it.

Equations

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

def Lean.Doc.OrderedListItemView.of (stx : TSyntax `Lean.Doc.Parser.ListItem.item) : Option OrderedListItemView

A view of stx, if it is an ordered list's item. Its marker must be a number.

Equations

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

structure Lean.Doc.DescItemView : Type

A view of an item description from a description list.

• stx : TSyntax `Lean.Doc.Parser.DescItem.item

  The original syntax.

• marker : Syntax

  The : that introduces the item.

• term : TSyntaxArray `Lean.Doc.Parser.inline

  The term that the item describes.

• desc : TSyntaxArray `Lean.Doc.Parser.block

  The description.

def Lean.Doc.DescItemView.of (stx : TSyntax `Lean.Doc.Parser.DescItem.item) : Option DescItemView

A view of stx, if it is a description list item.

Equations

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

structure Lean.Doc.ParaView : Type

A view of a paragraph.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• content : TSyntaxArray `Lean.Doc.Parser.inline

  The paragraph's contents.

@[instance_reducible]

instance Lean.Doc.instInhabitedParaView : Inhabited ParaView

Equations

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

def Lean.Doc.ParaView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option ParaView

A view of stx, if it is a paragraph.

Equations

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

structure Lean.Doc.UnorderedListView : Type

A view of an unordered list.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• items : Array UnorderedListItemView

  The list's items.

def Lean.Doc.UnorderedListView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option UnorderedListView

A view of stx, if it is an unordered list.

Equations

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

structure Lean.Doc.OrderedListView : Type

A view of an ordered list.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• start : Nat

  The number of the first item, which the first item's marker gives it.

• items : Array OrderedListItemView

  The list's items.

def Lean.Doc.OrderedListView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option OrderedListView

A view of stx, if it is an ordered list.

Equations

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

structure Lean.Doc.DescListView : Type

A view of a description list.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• items : Array DescItemView

  The list's items.

def Lean.Doc.DescListView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option DescListView

A view of stx, if it is a description list.

Equations

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

structure Lean.Doc.BlockquoteView : Type

A view of a block quotation.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• marker : Syntax

  The > that introduces the quotation.

• content : TSyntaxArray `Lean.Doc.Parser.block

  The quoted blocks.

def Lean.Doc.BlockquoteView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option BlockquoteView

A view of stx, if it is a block quotation.

Equations

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

structure Lean.Doc.CodeBlockView : Type

A view of a code block.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• openFence : TSyntax `Lean.Doc.Parser.codeBlockFence

  The opening run of backticks.

• name? : Option Ident

  The name that selects the code block's expander, where the code block invokes one.

• args : TSyntaxArray `Lean.Doc.Parser.arg

  The arguments to the expander.

• content : VersoCodeBlock

  The code.

• closeFence : TSyntax `Lean.Doc.Parser.codeBlockFence

  The closing run of backticks.

def Lean.Doc.CodeBlockView.getVersoCodeBlock (v : CodeBlockView) : String

The code, which is the texts of its lines in order.

Equations

• v.getVersoCodeBlock = Lean.TSyntax.getVersoCodeBlock v.content

def Lean.Doc.CodeBlockView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option CodeBlockView

A view of stx, if it is a code block.

Equations

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

structure Lean.Doc.DirectiveView : Type

A view of a directive.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• opener : TSyntax `Lean.Doc.Parser.directiveDelimiter

  The opening run of colons.

• name : Ident

  The name that selects the directive's expander.

• args : TSyntaxArray `Lean.Doc.Parser.arg

  The arguments to the directive.

• content : TSyntaxArray `Lean.Doc.Parser.block

  The blocks that the directive contains.

• closer : TSyntax `Lean.Doc.Parser.directiveDelimiter

  The closing run of colons.

def Lean.Doc.DirectiveView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option DirectiveView

A view of stx, if it is a directive.

Equations

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

structure Lean.Doc.CommandView : Type

A view of a block-level command.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• braceOpen : Syntax

  The { that opens the name and arguments.

• name : Ident

  The name that selects the command's expander.

• args : TSyntaxArray `Lean.Doc.Parser.arg

  The arguments to the command.

• braceClose : Syntax

  The } that closes the name and arguments.

def Lean.Doc.CommandView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option CommandView

A view of stx, if it is a block-level command.

Equations

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

structure Lean.Doc.HeaderView : Type

A view of a section header.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• marker : TSyntax `Lean.Doc.Parser.headerMarker

  The run of # characters.

• level : Nat

  The header's nesting depth, with 0 denoting a top-level header.

• content : TSyntaxArray `Lean.Doc.Parser.inline

  The header's text.

def Lean.Doc.HeaderView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option HeaderView

A view of stx, if it is a section header.

Equations

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

structure Lean.Doc.LinkRefView : Type

A view of a named URL that links and images can use.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• opener : Syntax

  The [ that opens the name.

• name : VersoRefName

  The name that a link or image uses to reach the URL.

• closer : Syntax

  The ]: that closes the name.

• url : VersoLinkRefUrl

  The URL.

def Lean.Doc.LinkRefView.getName (v : LinkRefView) : String

The name that a link or image repeats to reach this URL.

Equations

• v.getName = Lean.TSyntax.getVersoRefName v.name

def Lean.Doc.LinkRefView.getUrl (v : LinkRefView) : String

The URL that the reference provides.

Equations

• v.getUrl = Lean.TSyntax.getVersoLinkRefUrl v.url

def Lean.Doc.LinkRefView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option LinkRefView

A view of stx, if it is a named URL.

Equations

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

structure Lean.Doc.FootnoteRefView : Type

A view of a footnote definition.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• opener : Syntax

  The [^ that opens the name.

• name : VersoRefName

  The name of the footnote.

• closer : Syntax

  The ]: that closes the name.

• content : TSyntaxArray `Lean.Doc.Parser.inline

  The footnote's text.

def Lean.Doc.FootnoteRefView.getName (v : FootnoteRefView) : String

The name of the footnote.

Equations

• v.getName = Lean.TSyntax.getVersoRefName v.name

def Lean.Doc.FootnoteRefView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option FootnoteRefView

A view of stx, if it is a footnote definition.

Equations

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

structure Lean.Doc.MetadataView : Type

A view of a metadata block for the preceding header.

• stx : TSyntax `Lean.Doc.Parser.block

  The original syntax.

• opener : Syntax

  The opening %%%.

• contents : TSyntax `Lean.Parser.Term.structInstFields

  The metadata, written as the fields of a Lean structure instance.

• closer : Syntax

  The closing %%%.

def Lean.Doc.MetadataView.fields (v : MetadataView) : TSyntaxArray `Lean.Parser.Term.structInstField

The individual metadata fields, without their separators.

Equations

• v.fields = Array.map (fun (x : Lean.Syntax) => { raw := x }) v.contents.raw[0].getSepArgs

def Lean.Doc.MetadataView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option MetadataView

A view of stx, if it is a metadata block.

Equations

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

inductive Lean.Doc.BlockView : Type

A view of a block-level document element.

Each view records the syntax it is a view of, the delimiter atoms, and decoded values for literal content. Nested content stays as concrete syntax, for the consumer to view in turn.

• para (view : ParaView) : BlockView

  A paragraph.

• ul (view : UnorderedListView) : BlockView

  An unordered list.

• ol (view : OrderedListView) : BlockView

  An ordered list.

• dl (view : DescListView) : BlockView

  A description list.

• blockquote (view : BlockquoteView) : BlockView

  A block quotation.

• codeblock (view : CodeBlockView) : BlockView

  A code block.

• directive (view : DirectiveView) : BlockView

  A directive.

• command (view : CommandView) : BlockView

  A block-level command.

• header (view : HeaderView) : BlockView

  A section header.

• linkRef (view : LinkRefView) : BlockView

  A named URL that links and images can use.

• footnoteRef (view : FootnoteRefView) : BlockView

  A footnote definition.

• metadata (view : MetadataView) : BlockView

  A metadata block for the preceding header.

@[instance_reducible]

instance Lean.Doc.instInhabitedBlockView : Inhabited BlockView

Equations

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

@[instance_reducible]

instance Lean.Doc.instCoeParaViewBlockView : Coe ParaView BlockView

Equations

• Lean.Doc.instCoeParaViewBlockView = { coe := Lean.Doc.BlockView.para }

@[instance_reducible]

instance Lean.Doc.instCoeUnorderedListViewBlockView : Coe UnorderedListView BlockView

Equations

• Lean.Doc.instCoeUnorderedListViewBlockView = { coe := Lean.Doc.BlockView.ul }

@[instance_reducible]

instance Lean.Doc.instCoeOrderedListViewBlockView : Coe OrderedListView BlockView

Equations

• Lean.Doc.instCoeOrderedListViewBlockView = { coe := Lean.Doc.BlockView.ol }

@[instance_reducible]

instance Lean.Doc.instCoeDescListViewBlockView : Coe DescListView BlockView

Equations

• Lean.Doc.instCoeDescListViewBlockView = { coe := Lean.Doc.BlockView.dl }

@[instance_reducible]

instance Lean.Doc.instCoeBlockquoteViewBlockView : Coe BlockquoteView BlockView

Equations

• Lean.Doc.instCoeBlockquoteViewBlockView = { coe := Lean.Doc.BlockView.blockquote }

@[instance_reducible]

instance Lean.Doc.instCoeCodeBlockViewBlockView : Coe CodeBlockView BlockView

Equations

• Lean.Doc.instCoeCodeBlockViewBlockView = { coe := Lean.Doc.BlockView.codeblock }

@[instance_reducible]

instance Lean.Doc.instCoeDirectiveViewBlockView : Coe DirectiveView BlockView

Equations

• Lean.Doc.instCoeDirectiveViewBlockView = { coe := Lean.Doc.BlockView.directive }

@[instance_reducible]

instance Lean.Doc.instCoeCommandViewBlockView : Coe CommandView BlockView

Equations

• Lean.Doc.instCoeCommandViewBlockView = { coe := Lean.Doc.BlockView.command }

@[instance_reducible]

instance Lean.Doc.instCoeHeaderViewBlockView : Coe HeaderView BlockView

Equations

• Lean.Doc.instCoeHeaderViewBlockView = { coe := Lean.Doc.BlockView.header }

@[instance_reducible]

instance Lean.Doc.instCoeLinkRefViewBlockView : Coe LinkRefView BlockView

Equations

• Lean.Doc.instCoeLinkRefViewBlockView = { coe := Lean.Doc.BlockView.linkRef }

@[instance_reducible]

instance Lean.Doc.instCoeFootnoteRefViewBlockView : Coe FootnoteRefView BlockView

Equations

• Lean.Doc.instCoeFootnoteRefViewBlockView = { coe := Lean.Doc.BlockView.footnoteRef }

@[instance_reducible]

instance Lean.Doc.instCoeMetadataViewBlockView : Coe MetadataView BlockView

Equations

• Lean.Doc.instCoeMetadataViewBlockView = { coe := Lean.Doc.BlockView.metadata }

def Lean.Doc.BlockView.stx : BlockView → TSyntax `Lean.Doc.Parser.block

Returns the syntax underlying a block view.

Equations

• (Lean.Doc.BlockView.para v).stx = v.stx
• (Lean.Doc.BlockView.ul v).stx = v.stx
• (Lean.Doc.BlockView.ol v).stx = v.stx
• (Lean.Doc.BlockView.dl v).stx = v.stx
• (Lean.Doc.BlockView.blockquote v).stx = v.stx
• (Lean.Doc.BlockView.codeblock v).stx = v.stx
• (Lean.Doc.BlockView.directive v).stx = v.stx
• (Lean.Doc.BlockView.command v).stx = v.stx
• (Lean.Doc.BlockView.header v).stx = v.stx
• (Lean.Doc.BlockView.linkRef v).stx = v.stx
• (Lean.Doc.BlockView.footnoteRef v).stx = v.stx
• (Lean.Doc.BlockView.metadata v).stx = v.stx

def Lean.Doc.BlockView.of (stx : TSyntax `Lean.Doc.Parser.block) : Option BlockView

A view of stx, if it is a block-level document element.

Each production has a view of its own, and this tries them in turn. The productions have distinct syntax kinds, so at most one applies and the order does not matter.

Equations

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

def Lean.Doc.VersoInline.view (stx : VersoInline) : InlineView

Returns a view of an inline element of a Verso document.

Returns default if the syntax is malformed.

Equations

• stx.view = (Lean.Doc.InlineView.of stx).getD default

def Lean.Doc.VersoBlock.view (stx : VersoBlock) : BlockView

Returns a view of a block-level element of a Verso document.

Returns default if the syntax is malformed.

Equations

• stx.view = (Lean.Doc.BlockView.of stx).getD default