def Lean.validateDocComment {m : Type → Type} [Monad m] [MonadLiftT IO m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (docstring : TSyntax `Lean.Parser.Command.docComment) : m Unit

Validates all links to the Lean reference manual in docstring.

This is intended to be used before saving a docstring that is later subject to rewriting with rewriteManualLinks.

Equations

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

inductive Lean.VersoDocstringMarkup : Type

The markup of a Verso doc comment.

Parsing may have succeeded or failed, and the two cases are distinct.

Lean's docstring parser records an error in Verso syntax as a parse failure node rather than emitting a failure so that syntax errors in docstrings don't break processing of their associated definitions.

• document (doc : Doc.VersoDocument) : VersoDocstringMarkup

  Markup that parsed.

• parseFailure (text : Syntax) : VersoDocstringMarkup

  Markup that did not parse. text is the content that was actually sent to the parser, excluding opening and closing docstring delimiters.

def Lean.VersoDocstringMarkup.stx : VersoDocstringMarkup → Syntax

The syntax that covers the markup, whether or not it parsed.

Equations

• (Lean.VersoDocstringMarkup.document doc).stx = doc.raw
• (Lean.VersoDocstringMarkup.parseFailure text).stx = text

structure Lean.VersoDocstringView : Type

A view of a Verso doc comment: its delimiters and the markup between them.

• opener : Syntax

  The token that opens the comment.

• markup : VersoDocstringMarkup

  The markup between the delimiters.

• closer : Syntax

  The token that closes the comment.

def Lean.VersoDocstringView.of (docComment : TSyntax [`Lean.Parser.Command.docComment, `Lean.Parser.Command.moduleDoc]) : VersoDocstringView

Views a Verso documentation comment as its delimiters and the markup between them.

The comment's body must have been parsed as Verso markup, which isVersoDocComment reports.

Equations

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

def Lean.parseVersoDocStringAt (openPos startPos endPos : String.Pos.Raw) : CoreM (Option Doc.VersoDocument)

Parses the Verso docstring in the current file whose comment opens at openPos and whose contents are between startPos and endPos. Returns the document if it parsed, and otherwise logs each parse error.

Equations

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

def Lean.parseVersoDocString (docComment : TSyntax [`Lean.Parser.Command.docComment, `Lean.Parser.Command.moduleDoc]) : CoreM (Option Doc.VersoDocument)

Parses a docstring as Verso, returning the syntax if successful.

When not successful, parser errors are logged.

Equations

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

def Lean.reportVersoParseFailure (view : VersoDocstringView) : CoreM Unit

Reports parse errors from a Verso docstring parse failure.

When Verso docstring parsing fails at parse time, a parseFailure node is created containing the raw text, because emitting an error at that stage could lead to unwanted parser backtracking. This function reports the actual error messages with proper source positions.

Equations

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

structure Lean.VersoDocResult extends Lean.VersoDocString : Type

The result of elaborating a Verso docstring, which consists of the docstring contents paired with a set of deferred checks.

• text : Array (Doc.Block ElabInline ElabBlock)
• subsections : Array (Doc.Part ElabInline ElabBlock Empty)
• deferredChecks : Array Doc.DeferredCheck

  Checks that cannot be carried out during elaboration, typically because they require information that is not yet available.

def Lean.versoDocStringOfText (declName : Name) (binders : Syntax) (docComment : String) : Elab.TermElabM VersoDocResult

Parses a Verso docstring from its text and elaborates it for the specified declaration. Because the text carries no source positions, interactive features are disabled and any messages are reported at the current reference.

binders should be the syntax of the parameters to the constant that is being documented, as a null node that contains a sequence of bracketed binders, or an empty null node when none are available.

Equations

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

def Lean.versoDocString (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) : Elab.TermElabM VersoDocResult

Elaborates a Verso docstring for the specified declaration, which should already be present in the environment.

binders should be the syntax of the parameters to the constant that is being documented, as a null node that contains a sequence of bracketed binders. It is used to allow interactive features such as document highlights and “find references” to work for documented parameters. If no parameter binders are available, pass Syntax.missing or an empty null node.

Equations

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

def Lean.versoModDocString (range : DeclarationRange) (doc : Doc.VersoDocument) : Elab.TermElabM (VersoModuleDocs.Snippet × Array Doc.DeferredCheck)

Parses and elaborates a Verso module docstring.

Equations

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

def Lean.versoDocStringFromString (declName : Name) (docComment : String) : Elab.TermElabM VersoDocResult

Adds a Verso docstring to the specified declaration, which should already be present in the environment. The docstring is added from a string value, rather than syntax, which means that the interactive features are disabled.

Equations

• Lean.versoDocStringFromString declName docComment = Lean.versoDocStringOfText declName (Lean.mkNullNode #[]) docComment

def Lean.addMarkdownDocString {m : Type → Type} [Monad m] [MonadLiftT IO m] [MonadOptions m] [MonadEnv m] [MonadError m] [MonadLog m] [AddMessageContext m] (declName : Name) (docComment : TSyntax `Lean.Parser.Command.docComment) : m Unit

Adds a Markdown docstring to the environment, validating documentation links.

Equations

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

def Lean.addVersoDocStringCore {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadError m] (declName : Name) (docs : VersoDocString) (deferred : Array Doc.DeferredCheck) : m Unit

Adds an elaborated Verso docstring to the environment, recording its deferred checks under this declaration as their site.

Equations

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

def Lean.addVersoModDocStringCore {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadError m] (docs : VersoModuleDocs.Snippet) (deferred : Array Doc.DeferredCheck) : m Unit

Adds an elaborated Verso module docstring to the environment.

Equations

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

def Lean.addVersoDocString (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) : Elab.TermElabM Unit

Adds a Verso docstring to the environment.

binders should be the syntax of the parameters to the constant that is being documented, as a null node that contains a sequence of bracketed binders. It is used to allow interactive features such as document highlights and “find references” to work for documented parameters. If no parameter binders are available, pass Syntax.missing or an empty null node.

Equations

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

def Lean.addVersoDocStringFromString (declName : Name) (docComment : String) : Elab.TermElabM Unit

Adds a Verso docstring to the environment from a string value, which disables the interactive features. This should be used for programs that add documentation when there is no syntax available.

Equations

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

def Lean.addDocStringOf (isVerso : Bool) (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) : Elab.TermElabM Unit

Adds a docstring to the environment. If isVerso is false, then the docstring is interpreted as Markdown.

Equations

• Lean.addDocStringOf isVerso declName binders docComment = if isVerso = true then Lean.addVersoDocString declName binders docComment else Lean.addMarkdownDocString declName docComment

def Lean.makeDocStringVerso (declName : Name) : Elab.TermElabM Unit

Interprets a docstring that has been saved as a Markdown string as Verso, elaborating it. This is used during bootstrapping.

Equations

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

def Lean.addDocString (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) : Elab.TermElabM Unit

Adds a docstring to the environment.

Whether the docstring is processed as Verso or as Markdown is determined by the form of its syntax tree. To explicitly control whether the docstring is in Verso format, use addDocStringOf instead.

Markdown docstrings have their documentation links validated.

For Verso docstrings, binders should be the syntax of the parameters to the constant that is being documented, as a null node that contains a sequence of bracketed binders. It is used to allow interactive features such as document highlights and “find references” to work for documented parameters. If no parameter binders are available, pass Syntax.missing or an empty null node. binders is not used for Markdown docstrings.

Equations

• Lean.addDocString declName binders docComment = Lean.addDocStringOf (Lean.isVersoDocComment docComment) declName binders docComment

def Lean.addDocString' (declName : Name) (binders : Syntax) (docString? : Option (TSyntax `Lean.Parser.Command.docComment)) : Elab.TermElabM Unit

Adds a docstring to the environment, if it is provided. If no docstring is provided, nothing happens.

Whether the docstring is processed as Verso or as Markdown is determined by its syntax tree, which reflects the doc.verso option at the docstring's parse site. To explicitly control whether the docstring is in Verso format, use addDocStringOf instead.

Markdown docstrings have their documentation links validated.

For Verso docstrings, binders should be the syntax of the parameters to the constant that is being documented, as a null node that contains a sequence of bracketed binders. It is used to allow interactive features such as document highlights and “find references” to work for documented parameters. If no parameter binders are available, pass Syntax.missing or an empty null node. binders is not used for Markdown docstrings.

Equations

• Lean.addDocString' declName binders (some docString) = Lean.addDocString declName binders docString
• Lean.addDocString' declName binders none = pure ()

def Lean.addVersoModDocString (range : DeclarationRange) (doc : Doc.VersoDocument) : Elab.TermElabM Unit

Adds a Verso module docstring to the environment.

Equations

• Lean.addVersoModDocString range doc = do let __x ← Lean.versoModDocString range doc match __x with | (snippet, deferred) => Lean.addVersoModDocStringCore snippet deferred