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.

def Lean.parseVersoDocString {m : Type → Type} [Monad m] [MonadFileMap m] [MonadError m] [MonadEnv m] [MonadOptions m] [MonadLog m] [MonadResolveName m] (docComment : TSyntax [`Lean.Parser.Command.docComment, `Lean.Parser.Command.moduleDoc]) : m (Option Syntax)

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.versoDocString (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) : Elab.TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty))

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 : TSyntax `Lean.Doc.Parser.document) : Elab.TermElabM VersoModuleDocs.Snippet

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 (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty))

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

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

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) : m Unit

Adds an elaborated Verso docstring to the environment.

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) : 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.

If the option doc.verso is true, the docstring is processed as a Verso docstring. Otherwise, it is considered a Markdown docstring, and documentation links are validated. To explicitly control whether the docstring is in Verso format, use addDocStringOf instead.

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 = do let __do_lift ← Lean.getOptions Lean.addDocStringOf (Lean.Option.get __do_lift Lean.doc.verso) 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.

If the option doc.verso is true, the docstring is processed as a Verso docstring. Otherwise, it is considered a Markdown docstring, and documentation links are validated. To explicitly control whether the docstring is in Verso format, use addDocStringOf instead.

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) (docComment : TSyntax `Lean.Doc.Parser.document) : 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

• Lean.addVersoModDocString range docComment = do let snippet ← Lean.versoModDocString range docComment Lean.addVersoModDocStringCore snippet