opaque Lean.docStringExt : Lean.MapDeclarationExtension String

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

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

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

Equations

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

def Lean.findSimpleDocString? (env : Lean.Environment) (declName : Lean.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.

Equations

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

structure Lean.ModuleDoc : Type

• doc : String
• declarationRange : Lean.DeclarationRange

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

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

Equations

• Lean.getMainModuleDoc env = Lean.moduleDocExt✝.getState env

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

Equations

• Lean.getModuleDoc? env moduleName = Option.map (fun (modIdx : Lean.ModuleIdx) => Lean.PersistentEnvExtension.getModuleEntries Lean.moduleDocExt✝ env modIdx) (env.getModuleIdx? moduleName)

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

Equations

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