@[inline, reducible]

abbrev ImportCompletion.ImportTrie : Type

Equations

• ImportCompletion.ImportTrie = Lean.NameTrie Lake.Name

@[inline, reducible]

abbrev ImportCompletion.AvailableImports : Type

Equations

• ImportCompletion.AvailableImports = Array Lake.Name

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

Equations

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

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

Equations

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

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

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

Equations

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

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 Lake.Name

Equations

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

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

Equations

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

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

Equations

• ImportCompletion.computeCompletions text headerStx params = do let availableImports ← ImportCompletion.collectAvailableImports pure (ImportCompletion.find text headerStx params availableImports)