source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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

Instances For

source
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.

Instances For

source
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

Instances For

source
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 ()

Instances For

source
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

Instances For