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

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

Instances For

source
def Lean.Server.FileWorker.waitAllUnknownIdentifierMessageRanges (doc : EditableDocument) :
BaseIO (Array String.Range)
Equations

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

Instances For

source
structure Lean.Server.FileWorker.Insertion :
Type

- fullName : Name
- edit : Lsp.TextEdit

Instances For

source
structure Lean.Server.FileWorker.Query extends Lean.Lsp.LeanModuleQuery :
Type

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Server.FileWorker.importAllUnknownIdentifiersProvider :
Name
Equations

- Lean.Server.FileWorker.importAllUnknownIdentifiersProvider = `unknownIdentifiers

Instances For

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

Instances For

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

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

Instances For

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

Instances For