structure Lean.Server.FileWorker.UnknownIdentifierInfo : Type

• paramsRange : String.Range
• diagRange : String.Range

def Lean.Server.FileWorker.waitUnknownIdentifierRanges (doc : EditableDocument) (requestedRange : String.Range) : BaseIO (Array String.Range)

Equations

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

def Lean.Server.FileWorker.waitAllUnknownIdentifierRanges (doc : EditableDocument) : BaseIO (Array String.Range)

Equations

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

structure Lean.Server.FileWorker.Insertion : Type

• fullName : Name
• edit : Lsp.TextEdit

structure Lean.Server.FileWorker.Queryextends Lean.Lsp.LeanModuleQuery : Type

• identifier : String
• openNamespaces : Array OpenNamespace
• env : Environment
• determineInsertion : Name → Insertion

def Lean.Server.FileWorker.collectOpenNamespaces (currentNamespace : Name) (openDecls : List OpenDecl) : Array Lsp.OpenNamespace

Equations

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

def Lean.Server.FileWorker.computeIdQuery? (doc : EditableDocument) (ctx : Elab.ContextInfo) (stx : Syntax) (id : Name) : Option Query

Equations

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

def Lean.Server.FileWorker.computeDotQuery? (doc : EditableDocument) (ctx : Elab.ContextInfo) (ti : Elab.TermInfo) : IO (Option Query)

Equations

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

def Lean.Server.FileWorker.computeDotIdQuery? (doc : EditableDocument) (ctx : Elab.ContextInfo) (stx : Syntax) (id : Name) (lctx : LocalContext) (expectedType? : Option Expr) : IO (Option Query)

Equations

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

def Lean.Server.FileWorker.computeQueries (doc : EditableDocument) (requestedPos : String.Pos) : RequestM (Array Query)

Equations

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

def Lean.Server.FileWorker.importAllUnknownIdentifiersProvider : Name

Equations

• Lean.Server.FileWorker.importAllUnknownIdentifiersProvider = `unknownIdentifiers

def Lean.Server.FileWorker.importAllUnknownIdentifiersCodeAction (params : Lsp.CodeActionParams) (kind : String) : Lsp.CodeAction

Equations

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

def Lean.Server.FileWorker.handleUnknownIdentifierCodeAction (id : JsonRpc.RequestID) (params : Lsp.CodeActionParams) (requestedRange : String.Range) : RequestM (Array Lsp.CodeAction)

Equations

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

def Lean.Server.FileWorker.handleResolveImportAllUnknownIdentifiersCodeAction? (id : JsonRpc.RequestID) (action : Lsp.CodeAction) (unknownIdentifierRanges : Array String.Range) : RequestM (Option Lsp.CodeAction)

Equations

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