@[reducible, inline]

abbrev ImportCompletion.ImportTrie : Type

Equations

• ImportCompletion.ImportTrie = Lean.NameTrie Lean.Name

@[reducible, inline]

abbrev ImportCompletion.AvailableImports : Type

Equations

• ImportCompletion.AvailableImports = Array Lean.Name

def ImportCompletion.AvailableImports.toImportTrie (imports : ImportCompletion.AvailableImports) : ImportCompletion.ImportTrie

def ImportCompletion.determinePartialHeaderCompletions (headerStx : Lean.Syntax) (completionPos : String.Pos) : Option Lean.Syntax

def ImportCompletion.isImportNameCompletionRequest (headerStx : Lean.Syntax) (completionPos : String.Pos) : Bool

Checks whether completionPos points at the position after an incomplete import statement.

def ImportCompletion.isImportCmdCompletionRequest (headerStx : Lean.Syntax) (completionPos : String.Pos) : Bool

Checks whether completionPos points at a free space in the header.

Equations

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

def ImportCompletion.computePartialImportCompletions (headerStx : Lean.Syntax) (completionPos : String.Pos) (availableImports : ImportCompletion.ImportTrie) : Array Lean.Name

def ImportCompletion.isImportCompletionRequest (text : Lean.FileMap) (headerStx : Lean.Syntax) (params : Lean.Lsp.CompletionParams) : Bool

Equations

• ImportCompletion.isImportCompletionRequest text headerStx params = decide (text.lspPosToUtf8Pos params.position ≤ headerStx.getTailPos?.getD (headerStx.getPos?.getD 0) + ' ' + ' ')

def ImportCompletion.collectAvailableImportsFromLake : IO (Option ImportCompletion.AvailableImports)

Equations

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

def ImportCompletion.collectAvailableImportsFromSrcSearchPath : IO ImportCompletion.AvailableImports

Equations

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

def ImportCompletion.collectAvailableImports : IO ImportCompletion.AvailableImports

Equations

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

def ImportCompletion.addCompletionItemData (completionList : Lean.Lsp.CompletionList) (params : Lean.Lsp.CompletionParams) : Lean.Lsp.CompletionList

Sets the data? field of every CompletionItem in completionList using params. Ensures that completionItem/resolve requests can be routed to the correct file worker even for CompletionItems produced by the import completion.

def ImportCompletion.find (text : Lean.FileMap) (headerStx : Lean.Syntax) (params : Lean.Lsp.CompletionParams) (availableImports : ImportCompletion.AvailableImports) : Lean.Lsp.CompletionList

Equations

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

def ImportCompletion.computeCompletions (text : Lean.FileMap) (headerStx : Lean.Syntax) (params : Lean.Lsp.CompletionParams) : IO Lean.Lsp.CompletionList