Documentation
Lean
.
Server
.
FileSource
Search
Google site search
Lean
.
Server
.
FileSource
source
Imports
Init
Lean.Data.Lsp
Imported by
Lean
.
Lsp
.
FileSource
Lean
.
Lsp
.
instFileSourceLocation
Lean
.
Lsp
.
instFileSourceTextDocumentIdentifier
Lean
.
Lsp
.
instFileSourceVersionedTextDocumentIdentifier
Lean
.
Lsp
.
instFileSourceTextDocumentEdit
Lean
.
Lsp
.
instFileSourceTextDocumentItem
Lean
.
Lsp
.
instFileSourceTextDocumentPositionParams
Lean
.
Lsp
.
instFileSourceDidOpenTextDocumentParams
Lean
.
Lsp
.
instFileSourceDidChangeTextDocumentParams
Lean
.
Lsp
.
instFileSourceDidCloseTextDocumentParams
Lean
.
Lsp
.
instFileSourceCompletionParams
Lean
.
Lsp
.
instFileSourceHoverParams
Lean
.
Lsp
.
instFileSourceDeclarationParams
Lean
.
Lsp
.
instFileSourceDefinitionParams
Lean
.
Lsp
.
instFileSourceTypeDefinitionParams
Lean
.
Lsp
.
instFileSourceReferenceParams
Lean
.
Lsp
.
instFileSourceWaitForDiagnosticsParams
Lean
.
Lsp
.
instFileSourceDocumentHighlightParams
Lean
.
Lsp
.
instFileSourceDocumentSymbolParams
Lean
.
Lsp
.
instFileSourceSemanticTokensParams
Lean
.
Lsp
.
instFileSourceSemanticTokensRangeParams
Lean
.
Lsp
.
instFileSourceFoldingRangeParams
Lean
.
Lsp
.
instFileSourcePlainGoalParams
Lean
.
Lsp
.
instFileSourcePlainTermGoalParams
Lean
.
Lsp
.
instFileSourceRpcConnectParams
Lean
.
Lsp
.
instFileSourceRpcCallParams
Lean
.
Lsp
.
instFileSourceRpcReleaseParams
Lean
.
Lsp
.
instFileSourceRpcKeepAliveParams
Lean
.
Lsp
.
instFileSourceCodeActionParams
source
class
Lean
.
Lsp
.
FileSource
(α :
Type
)
:
Type
fileSource :
α
→
Lean.Lsp.DocumentUri
Instances
source
instance
Lean
.
Lsp
.
instFileSourceLocation
:
Lean.Lsp.FileSource
Lean.Lsp.Location
source
instance
Lean
.
Lsp
.
instFileSourceTextDocumentIdentifier
:
Lean.Lsp.FileSource
Lean.Lsp.TextDocumentIdentifier
source
instance
Lean
.
Lsp
.
instFileSourceVersionedTextDocumentIdentifier
:
Lean.Lsp.FileSource
Lean.Lsp.VersionedTextDocumentIdentifier
source
instance
Lean
.
Lsp
.
instFileSourceTextDocumentEdit
:
Lean.Lsp.FileSource
Lean.Lsp.TextDocumentEdit
source
instance
Lean
.
Lsp
.
instFileSourceTextDocumentItem
:
Lean.Lsp.FileSource
Lean.Lsp.TextDocumentItem
source
instance
Lean
.
Lsp
.
instFileSourceTextDocumentPositionParams
:
Lean.Lsp.FileSource
Lean.Lsp.TextDocumentPositionParams
source
instance
Lean
.
Lsp
.
instFileSourceDidOpenTextDocumentParams
:
Lean.Lsp.FileSource
Lean.Lsp.DidOpenTextDocumentParams
source
instance
Lean
.
Lsp
.
instFileSourceDidChangeTextDocumentParams
:
Lean.Lsp.FileSource
Lean.Lsp.DidChangeTextDocumentParams
source
instance
Lean
.
Lsp
.
instFileSourceDidCloseTextDocumentParams
:
Lean.Lsp.FileSource
Lean.Lsp.DidCloseTextDocumentParams
source
instance
Lean
.
Lsp
.
instFileSourceCompletionParams
:
Lean.Lsp.FileSource
Lean.Lsp.CompletionParams
source
instance
Lean
.
Lsp
.
instFileSourceHoverParams
:
Lean.Lsp.FileSource
Lean.Lsp.HoverParams
source
instance
Lean
.
Lsp
.
instFileSourceDeclarationParams
:
Lean.Lsp.FileSource
Lean.Lsp.DeclarationParams
source
instance
Lean
.
Lsp
.
instFileSourceDefinitionParams
:
Lean.Lsp.FileSource
Lean.Lsp.DefinitionParams
source
instance
Lean
.
Lsp
.
instFileSourceTypeDefinitionParams
:
Lean.Lsp.FileSource
Lean.Lsp.TypeDefinitionParams
source
instance
Lean
.
Lsp
.
instFileSourceReferenceParams
:
Lean.Lsp.FileSource
Lean.Lsp.ReferenceParams
source
instance
Lean
.
Lsp
.
instFileSourceWaitForDiagnosticsParams
:
Lean.Lsp.FileSource
Lean.Lsp.WaitForDiagnosticsParams
source
instance
Lean
.
Lsp
.
instFileSourceDocumentHighlightParams
:
Lean.Lsp.FileSource
Lean.Lsp.DocumentHighlightParams
source
instance
Lean
.
Lsp
.
instFileSourceDocumentSymbolParams
:
Lean.Lsp.FileSource
Lean.Lsp.DocumentSymbolParams
source
instance
Lean
.
Lsp
.
instFileSourceSemanticTokensParams
:
Lean.Lsp.FileSource
Lean.Lsp.SemanticTokensParams
source
instance
Lean
.
Lsp
.
instFileSourceSemanticTokensRangeParams
:
Lean.Lsp.FileSource
Lean.Lsp.SemanticTokensRangeParams
source
instance
Lean
.
Lsp
.
instFileSourceFoldingRangeParams
:
Lean.Lsp.FileSource
Lean.Lsp.FoldingRangeParams
source
instance
Lean
.
Lsp
.
instFileSourcePlainGoalParams
:
Lean.Lsp.FileSource
Lean.Lsp.PlainGoalParams
source
instance
Lean
.
Lsp
.
instFileSourcePlainTermGoalParams
:
Lean.Lsp.FileSource
Lean.Lsp.PlainTermGoalParams
source
instance
Lean
.
Lsp
.
instFileSourceRpcConnectParams
:
Lean.Lsp.FileSource
Lean.Lsp.RpcConnectParams
source
instance
Lean
.
Lsp
.
instFileSourceRpcCallParams
:
Lean.Lsp.FileSource
Lean.Lsp.RpcCallParams
source
instance
Lean
.
Lsp
.
instFileSourceRpcReleaseParams
:
Lean.Lsp.FileSource
Lean.Lsp.RpcReleaseParams
source
instance
Lean
.
Lsp
.
instFileSourceRpcKeepAliveParams
:
Lean.Lsp.FileSource
Lean.Lsp.RpcKeepAliveParams
source
instance
Lean
.
Lsp
.
instFileSourceCodeActionParams
:
Lean.Lsp.FileSource
Lean.Lsp.CodeActionParams