inductive Lean.ElabInline : Type

Saved data that describes a custom inline element.

The type of value contained within the Dynamic determines the interpretation of the custom element, including how it is rendered to Markdown for the language server.

• custom (val : Dynamic) : ElabInline

  A custom inline element. The type of the value in the Dynamic determines how it is interpreted and rendered.

• deferred (index : Nat) : ElabInline

  A deferred check that lacked sufficient information when it was used (e.g. a forward references to a name in a downstream module). The index identifies it among the docstring's deferred checks that are stored in an environment extension. Inline and block deferred checks use the same counter.

@[instance_reducible]

instance Lean.instReprElabInline : Repr ElabInline

inductive Lean.ElabBlock : Type

Saved data that describes a custom block element.

The type of value contained within the Dynamic determines the interpretation of the custom element, including how it is rendered to Markdown for the language server.

• custom (val : Dynamic) : ElabBlock

  A custom block element. The type of the value in the Dynamic determines how it is interpreted and rendered.

• deferred (index : Nat) : ElabBlock

  A deferred check that lacked sufficient information when it was used (e.g. a forward references to a name in a downstream module). The index identifies it among the docstring's deferred checks that are stored in an environment extension. Inline and block deferred checks use the same counter.

@[instance_reducible]

instance Lean.instReprElabBlock : Repr ElabBlock

@[inline]

def Lean.Doc.Inline.custom {α : Type u_1} [TypeName α] (val : α) (content : Array (Inline ElabInline)) : Inline ElabInline

A custom inline element val. The type α determines how it is interpreted. In contexts where α is not understood, content is used as a fallback.

@[inline]

def Lean.Doc.Inline.deferred (index : Nat) (content : Array (Inline ElabInline)) : Inline ElabInline

An inline element with a deferred check. The index is a 0-based index into the current docstring's deferred checks, in source order. Block and inline deferred elements share a counter.

@[inline]

def Lean.Doc.Block.custom {α : Type u_1} [TypeName α] (val : α) (content : Array (Block ElabInline ElabBlock)) : Block ElabInline ElabBlock

A custom block element val. The type α determines how it is interpreted. In contexts where α is not understood, content is used as a fallback.

@[inline]

def Lean.Doc.Block.deferred (index : Nat) (content : Array (Block ElabInline ElabBlock)) : Block ElabInline ElabBlock

A block element with a deferred check. The index is a 0-based index into the current docstring's deferred checks, in source order. Block and inline deferred elements share a counter.

structure Lean.VersoDocString : Type

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

@[instance_reducible]

instance Lean.instInhabitedVersoDocString : Inhabited 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.

The text should have already had its leading indentation removed by the caller.

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.throwIfHasDocString {m : Type → Type} [Monad m] [MonadError m] [MonadEnv m] (declName : Name) : m Unit

Throws if declName already has a Markdown or Verso docstring.

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

Sets the docstring of declName, replacing an existing one: metaprograms extend docstrings this way (e.g. by appending cross-reference links). Only add_decl_doc rejects a second docstring.

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

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.addInheritedDocString {m : Type → Type} [Monad m] [MonadError m] [MonadEnv m] [MonadLiftT IO m] (declName target : Name) : m Unit

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

def Lean.isVersoDocComment (stx : TSyntax `Lean.Parser.Command.docComment) : Bool

Checks whether stx is a docstring that was parsed as Verso rather than Markdown.

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.

@[instance_reducible]

instance Lean.VersoModuleDocs.instInhabitedSnippet : Inhabited Snippet

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

@[instance_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

structure Lean.VersoModuleDocs : Type

• snippets : PersistentArray Snippet

@[instance_reducible]

instance Lean.instInhabitedVersoModuleDocs : Inhabited VersoModuleDocs

def Lean.VersoModuleDocs.terminalNesting : VersoModuleDocs → Option Nat

@[instance_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