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

Equations

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

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

Equations

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

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

Equations

• Lean.Doc.Inline.custom val content = Lean.Doc.Inline.other (Lean.ElabInline.custom (Dynamic.mk val)) content

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

Equations

• Lean.Doc.Inline.deferred index content = Lean.Doc.Inline.other (Lean.ElabInline.deferred index) content

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

Equations

• Lean.Doc.Block.custom val content = Lean.Doc.Block.other (Lean.ElabBlock.custom (Dynamic.mk val)) content

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

Equations

• Lean.Doc.Block.deferred index content = Lean.Doc.Block.other (Lean.ElabBlock.deferred index) content

structure Lean.VersoDocString : Type

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

@[instance_reducible]

instance Lean.instInhabitedVersoDocString : Inhabited VersoDocString

Equations

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

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.

Equations

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

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

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

Equations

• Lean.removeBuiltinDocString declName = ST.Ref.modify Lean.builtinDocStrings✝ fun (x : Lean.NameMap String) => Std.TreeMap.erase x declName

def Lean.getBuiltinVersoDocStrings : IO (NameMap VersoDocString)

Retrieves all builtin Verso docstrings.

Equations

• Lean.getBuiltinVersoDocStrings = ST.Ref.get Lean.builtinVersoDocStrings✝

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.

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

Equations

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

def Lean.removeDocStringCore {m : Type → Type} [Monad m] [MonadError m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : 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 ()

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

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.

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

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

Equations

• Lean.isVersoDocComment stx = stx.raw[1].isOfKind `Lean.Parser.Command.versoCommentBody

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

Equations

• Lean.VersoModuleDocs.instInhabitedSnippet = { default := Lean.VersoModuleDocs.instInhabitedSnippet.default }

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

Equations

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

@[instance_reducible]

instance Lean.VersoModuleDocs.instReprSnippet : Repr Snippet

Equations

• Lean.VersoModuleDocs.instReprSnippet = { reprPrec := Lean.VersoModuleDocs.instReprSnippet.repr }

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

Equations

• Lean.VersoModuleDocs.Snippet.canNestIn level snippet = match snippet.sections[0]? with | some s => decide (s.fst ≤ level + 1) | x => true

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

Equations

• snippet.terminalNesting = match snippet.sections.back? with | some s => some s.fst | x => none

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

Equations

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

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

Equations

• snippet.addPart level range part = { text := snippet.text, sections := snippet.sections.push (level, range, part), declarationRange := snippet.declarationRange }

structure Lean.VersoModuleDocs : Type

• snippets : PersistentArray Snippet

@[instance_reducible]

instance Lean.instInhabitedVersoModuleDocs : Inhabited VersoModuleDocs

Equations

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

def Lean.VersoModuleDocs.terminalNesting : VersoModuleDocs → Option Nat

Equations

• { snippets := snippets }.terminalNesting = snippets.findSomeRev? fun (x : Lean.VersoModuleDocs.Snippet) => x.terminalNesting

@[instance_reducible]

instance Lean.instReprVersoModuleDocs : Repr VersoModuleDocs

Equations

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

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

Equations

• docs.isEmpty = docs.snippets.isEmpty

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

Equations

• docs.canAdd snippet = match docs.terminalNesting with | some level => Lean.VersoModuleDocs.Snippet.canNestIn level snippet | x => true

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

• Lean.getMainVersoModuleDocs env = Lean.versoModuleDocExt✝.getState env

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

def Lean.getVersoModuleDocs (env : Environment) : VersoModuleDocs

Equations

• Lean.getVersoModuleDocs = Lean.getMainVersoModuleDocs

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.

Equations

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

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

Equations

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