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.

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.

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

A view of stx, if it is an argument.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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

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

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

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

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

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

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

A view of stx, if it is ordinary text.

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.

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.

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

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

A view of stx, if it is inline code.

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.

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.

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.

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.

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

A view of stx, if it is an image.

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.

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

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

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.

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.

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

@[instance_reducible]

instance Lean.Doc.instCoeTextViewInlineView : Coe TextView InlineView

@[instance_reducible]

instance Lean.Doc.instCoeEmphViewInlineView : Coe EmphView InlineView

@[instance_reducible]

instance Lean.Doc.instCoeBoldViewInlineView : Coe BoldView InlineView

@[instance_reducible]

instance Lean.Doc.instCoeCodeViewInlineView : Coe CodeView InlineView

@[instance_reducible]

instance Lean.Doc.instCoeMathViewInlineView : Coe MathView InlineView

@[instance_reducible]

instance Lean.Doc.instCoeLinkViewInlineView : Coe LinkView InlineView

@[instance_reducible]

instance Lean.Doc.instCoeImageViewInlineView : Coe ImageView InlineView

@[instance_reducible]

instance Lean.Doc.instCoeFootnoteViewInlineView : Coe FootnoteView InlineView

@[instance_reducible]

instance Lean.Doc.instCoeLinebreakViewInlineView : Coe LinebreakView InlineView

@[instance_reducible]

instance Lean.Doc.instCoeRoleViewInlineView : Coe RoleView InlineView

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

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

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.

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.

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.

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.

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.

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

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

A view of stx, if it is a paragraph.

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.

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.

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.

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.

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.

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

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

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.

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.

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.

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.

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

The URL that the reference provides.

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

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

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.

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

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

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.

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

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

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

@[instance_reducible]

instance Lean.Doc.instCoeParaViewBlockView : Coe ParaView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeUnorderedListViewBlockView : Coe UnorderedListView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeOrderedListViewBlockView : Coe OrderedListView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeDescListViewBlockView : Coe DescListView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeBlockquoteViewBlockView : Coe BlockquoteView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeCodeBlockViewBlockView : Coe CodeBlockView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeDirectiveViewBlockView : Coe DirectiveView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeCommandViewBlockView : Coe CommandView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeHeaderViewBlockView : Coe HeaderView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeLinkRefViewBlockView : Coe LinkRefView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeFootnoteRefViewBlockView : Coe FootnoteRefView BlockView

@[instance_reducible]

instance Lean.Doc.instCoeMetadataViewBlockView : Coe MetadataView BlockView

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

Returns the syntax underlying a block view.

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.

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.

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.