def
Lean.validateDocComment
{m : Type → Type}
[Monad m]
[MonadLog m]
[AddMessageContext m]
[MonadOptions m]
[MonadLiftT IO 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.addDocString
{m : Type → Type}
[Monad m]
[MonadError m]
[MonadEnv m]
[MonadLog m]
[AddMessageContext m]
[MonadOptions m]
[MonadLiftT IO m]
(declName : Name)
(docComment : TSyntax `Lean.Parser.Command.docComment)
:
m Unit
Adds a docstring to the environment, validating documentation links.
Equations
- One or more equations did not get rendered due to their size.
def
Lean.addDocString'
{m : Type → Type}
[Monad m]
[MonadError m]
[MonadEnv m]
[MonadLog m]
[AddMessageContext m]
[MonadOptions m]
[MonadLiftT IO m]
(declName : Name)
(docString? : Option (TSyntax `Lean.Parser.Command.docComment))
:
m Unit
Adds a docstring to the environment, validating documentation links.
Equations
- Lean.addDocString' declName (some docString) = Lean.addDocString declName docString
- Lean.addDocString' declName none = pure ()