opaque Lean.docStringExt : MapDeclarationExtension String

def Lean.addBuiltinDocString (declName : Name) (docString : String) : IO Unit

Adds a builtin docstring to the compiler.

Links to the Lean manual aren't validated.

def Lean.addDocStringCore {m : Type → Type} [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit

def Lean.addDocStringCore' {m : Type → Type} [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit

def Lean.findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin : Bool := true) : IO (Option String)

Finds a docstring without performing any alias resolution or enrichment with extra metadata.

Docstrings to be shown to a user should be looked up with Lean.findDocString? instead.

structure Lean.ModuleDoc : Type

• doc : String
• declarationRange : DeclarationRange

def Lean.addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment

def Lean.getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc

def Lean.getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc)

def Lean.getDocStringText {m : Type → Type} [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String