source
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

Instances For

source
instance Lean.instReprElabInline :
Repr ElabInline
Equations

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

source
instance Lean.instMarkdownInlineElabInline :
Doc.MarkdownInline ElabInline
Equations

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

source
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

Instances For

source
instance Lean.instReprElabBlock :
Repr ElabBlock
Equations

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

source
instance Lean.instMarkdownBlockElabInlineElabBlock :
Doc.MarkdownBlock ElabInline ElabBlock
Equations

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

source
structure Lean.VersoDocString :
Type

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

Instances For

source
instance Lean.instInhabitedVersoDocString :
Inhabited VersoDocString
Equations

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

source
def Lean.instInhabitedVersoDocString.default :
VersoDocString
Equations

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

Instances For

source
opaque Lean.doc.verso :
Lean.Option Bool
source
opaque Lean.docStringExt :
MapDeclarationExtension String
source
opaque Lean.versoDocStringExt :
MapDeclarationExtension VersoDocString
source
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

Instances For

source
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

Instances For

source
def Lean.getBuiltinVersoDocStrings :
IO (NameMap VersoDocString)

Retrieves all builtin Verso docstrings.

Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

source
structure Lean.ModuleDoc :
Type

- doc : String
- declarationRange : DeclarationRange

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

source
def Lean.VersoModuleDocs.instInhabitedSnippet.default :
Snippet
Equations

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

Instances For

source
instance Lean.VersoModuleDocs.instInhabitedSnippet :
Inhabited Snippet
Equations

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

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

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

Instances For

source
instance Lean.VersoModuleDocs.instReprSnippet :
Repr Snippet
Equations

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

source
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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

source
instance Lean.instToMarkdownSnippet :
Doc.ToMarkdown VersoModuleDocs.Snippet
Equations

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

source
structure Lean.VersoModuleDocs :
Type

- snippets : PersistentArray Snippet
- terminalNesting : Option Nat

Instances For

source
instance Lean.instInhabitedVersoModuleDocs :
Inhabited VersoModuleDocs
Equations

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

source
def Lean.instInhabitedVersoModuleDocs.default :
VersoModuleDocs
Equations

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

Instances For

source
instance Lean.instReprVersoModuleDocs :
Repr VersoModuleDocs
Equations

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

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

- docs.isEmpty = docs.snippets.isEmpty

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.getVersoModuleDocs (env : Environment) :
VersoModuleDocs
Equations

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

Instances For

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

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

Instances For