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

@[implicit_reducible]

instance Lean.instReprElabInline : Repr ElabInline

@[implicit_reducible]

instance Lean.instMarkdownInlineElabInline : Doc.MarkdownInline ElabInline

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
• val : Dynamic

@[implicit_reducible]

instance Lean.instReprElabBlock : Repr ElabBlock

@[implicit_reducible]

instance Lean.instMarkdownBlockElabInlineElabBlock : Doc.MarkdownBlock ElabInline ElabBlock

structure Lean.VersoDocString : Type

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

@[implicit_reducible]

instance Lean.instInhabitedVersoDocString : Inhabited VersoDocString

def Lean.instInhabitedVersoDocString.default : VersoDocString

opaque Lean.doc.verso : Lean.Option Bool

opaque Lean.doc.verso.module : 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.

def Lean.removeBuiltinDocString (declName : Name) : IO Unit

Removes a builtin docstring from the compiler. This is used when translating between formats.

def Lean.getBuiltinVersoDocStrings : IO (NameMap VersoDocString)

Retrieves all builtin Verso docstrings.

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

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

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

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

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.

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

structure Lean.VersoModuleDocs.Snippet : Type

A snippet of a Verso module text.

A snippet consists of text followed by subsections. Because the sequence of snippets that occur in a source file are conceptually a single document, they have a consistent header nesting structure. This means that initial textual content of a snippet is a continuation of the text at the end of the prior snippet.

The actual hierarchical structure of the document is reconstructed from the sequence of snippets.

The terminal nesting of a sequence of snippets is 0 if there are no sections in the sequence. Otherwise, it is one greater than the nesting of the last snippet's last section. The module docstring elaborator maintains the invariant that each snippet's first section's level is at most the terminal nesting of the preceding snippets, and that the level of each section within a snippet is at most one greater than the preceding section's level.

• text : Array (Doc.Block ElabInline ElabBlock)

  Text to be inserted after the prior snippet's ending text.

• sections : Array (Nat × DeclarationRange × Doc.Part ElabInline ElabBlock Empty)

  A sequence of parts with their absolute document nesting levels and header positions. None of these parts may contain sub-parts.

• declarationRange : DeclarationRange

  The location of the snippet in the source file.

@[implicit_reducible]

instance Lean.VersoModuleDocs.instInhabitedSnippet : Inhabited Snippet

def Lean.VersoModuleDocs.instInhabitedSnippet.default : Snippet

def Lean.VersoModuleDocs.instReprSnippet.repr : Snippet → Nat → Format

@[implicit_reducible]

instance Lean.VersoModuleDocs.instReprSnippet : Repr Snippet

def Lean.VersoModuleDocs.Snippet.canNestIn (level : Nat) (snippet : Snippet) : Bool

def Lean.VersoModuleDocs.Snippet.terminalNesting (snippet : Snippet) : Option Nat

def Lean.VersoModuleDocs.Snippet.addBlock (snippet : Snippet) (block : Doc.Block ElabInline ElabBlock) : Snippet

def Lean.VersoModuleDocs.Snippet.addPart (snippet : Snippet) (level : Nat) (range : DeclarationRange) (part : Doc.Part ElabInline ElabBlock Empty) : Snippet

@[implicit_reducible]

instance Lean.instToMarkdownSnippet : Doc.ToMarkdown VersoModuleDocs.Snippet

structure Lean.VersoModuleDocs : Type

• snippets : PersistentArray Snippet
• terminalNesting : Option Nat

@[implicit_reducible]

instance Lean.instInhabitedVersoModuleDocs : Inhabited VersoModuleDocs

def Lean.instInhabitedVersoModuleDocs.default : VersoModuleDocs

@[implicit_reducible]

instance Lean.instReprVersoModuleDocs : Repr VersoModuleDocs

def Lean.VersoModuleDocs.isEmpty (docs : VersoModuleDocs) : Bool

def Lean.VersoModuleDocs.canAdd (docs : VersoModuleDocs) (snippet : Snippet) : Bool

def Lean.VersoModuleDocs.add (docs : VersoModuleDocs) (snippet : Snippet) : Except String VersoModuleDocs

def Lean.VersoModuleDocs.add! (docs : VersoModuleDocs) (snippet : Snippet) : VersoModuleDocs

def Lean.VersoModuleDocs.assemble (docs : VersoModuleDocs) : Except String VersoDocString

def Lean.getMainVersoModuleDocs (env : Environment) : VersoModuleDocs

Returns the Verso module docs for the current main module.

During elaboration, this will return the modules docs that have been added thus far, rather than those for the entire module.

@[deprecated Lean.getMainVersoModuleDocs (since := "2026-01-21")]

def Lean.getVersoModuleDocs (env : Environment) : VersoModuleDocs

def Lean.getVersoModuleDoc? (env : Environment) (moduleName : Name) : Option (Array VersoModuleDocs.Snippet)

Returns all snippets of the Verso module docs from the indicated module, if they exist.

def Lean.addVersoModuleDocSnippet (env : Environment) (snippet : VersoModuleDocs.Snippet) : Except String Environment