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

instance Lean.instReprElabInline : Repr ElabInline

Equations

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

instance Lean.instMarkdownInlineElabInline : Doc.MarkdownInline ElabInline

Equations

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

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

instance Lean.instReprElabBlock : Repr ElabBlock

Equations

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

instance Lean.instMarkdownBlockElabInlineElabBlock : Doc.MarkdownBlock ElabInline ElabBlock

Equations

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

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.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.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.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 ()

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.

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.

def Lean.VersoModuleDocs.instInhabitedSnippet.default : Snippet

Equations

• Lean.VersoModuleDocs.instInhabitedSnippet.default = { text := default, sections := default, declarationRange := default }

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 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 }

instance Lean.instToMarkdownSnippet : Doc.ToMarkdown VersoModuleDocs.Snippet

Equations

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

structure Lean.VersoModuleDocs : Type

• snippets : PersistentArray Snippet
• terminalNesting : Option Nat

instance Lean.instInhabitedVersoModuleDocs : Inhabited VersoModuleDocs

Equations

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

def Lean.instInhabitedVersoModuleDocs.default : VersoModuleDocs

Equations

• Lean.instInhabitedVersoModuleDocs.default = { snippets := default, terminalNesting := default }

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.getVersoModuleDocs (env : Environment) : VersoModuleDocs

Equations

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

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

Equations

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