def Lean.Server.FileWorker.waitUnknownIdentifierRanges (doc : EditableDocument) (requestedRange : Syntax.Range) : BaseIO (Array Syntax.Range × Bool)

Equations

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

def Lean.Server.FileWorker.waitAllUnknownIdentifierMessageRanges (doc : EditableDocument) : BaseIO (Array Syntax.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.Query extends Lean.Lsp.LeanModuleQuery : Type

• identifier : String
• openNamespaces : Array OpenNamespace
• ctx : Elab.ContextInfo
• 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.Raw) : 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 = `allUnknownIdentifiers

def Lean.Server.FileWorker.importUnknownIdentifiersProvider : Name

Equations

• Lean.Server.FileWorker.importUnknownIdentifiersProvider = `unknownIdentifiers

def Lean.Server.FileWorker.mkUnknownIdentifierCodeActionData (params : Lsp.CodeActionParams) (name : Name := importUnknownIdentifiersProvider) : CodeActionResolveData

Equations

• Lean.Server.FileWorker.mkUnknownIdentifierCodeActionData params name = { params := params, providerName := name, providerResultIndex := 0 }

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 : Syntax.Range) (kind : String) : 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 Syntax.Range) : RequestM (Option Lsp.CodeAction)

Equations

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