structure Lean.ElabInline : Type

Saved data that describes the contents. The name should determine both the type of the value and its interpretation; if in doubt, use the name of the elaborator that produces the data.

• name : Name
• val : Dynamic

structure Lean.ElabBlock : Type

Saved data that describes the contents. The name should determine both the type of the value and its interpretation; if in doubt, use the name of the elaborator that produces the data.

• name : Name
• value : Dynamic

structure Lean.VersoDocString : Type

• text : Array (Doc.Block ElabInline ElabBlock)
• subsections : Array (Doc.Part ElabInline ElabBlock Empty)

instance Lean.instInhabitedVersoDocString : Inhabited VersoDocString

Equations

• Lean.instInhabitedVersoDocString = { default := Lean.instInhabitedVersoDocString.default }

def Lean.instInhabitedVersoDocString.default : VersoDocString

Equations

• Lean.instInhabitedVersoDocString.default = { text := default, subsections := default }

opaque Lean.doc.verso : Lean.Option Bool

opaque Lean.docStringExt : MapDeclarationExtension String

opaque Lean.versoDocStringExt : MapDeclarationExtension VersoDocString

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

Adds a builtin docstring to the compiler.

Links to the Lean manual aren't validated.

Equations

• Lean.addBuiltinDocString declName docString = ST.Ref.modify Lean.builtinDocStrings✝ fun (x : Lean.NameMap String) => x.insert declName docString.removeLeadingSpaces

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

Equations

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

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

Equations

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

def Lean.addInheritedDocString {m : Type → Type} [Monad m] [MonadError m] [MonadEnv m] (declName target : Name) : m Unit

Equations

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

partial def Lean.findInternalDocString? (env : Environment) (declName : Name) (includeBuiltin : Bool := true) : IO (Option (String ⊕ VersoDocString))

Finds a docstring without performing any alias resolution or enrichment with extra metadata. For Markdown docstrings, the result is a string; for Verso docstrings, it's a VersoDocString.

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

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. The result is rendered as Markdown.

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 : DeclarationRange

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

Equations

• Lean.addMainModuleDoc env doc = Lean.PersistentEnvExtension.addEntry Lean.moduleDocExt✝ env doc

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

Equations

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

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

Equations

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

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

Equations

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