class Lean.Lsp.FileSource (α : Type) : Type

• fileSource : α → DocumentUri

instance Lean.Lsp.instFileSourceLocation : FileSource Location

instance Lean.Lsp.instFileSourceTextDocumentIdentifier : FileSource TextDocumentIdentifier

instance Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier : FileSource VersionedTextDocumentIdentifier

instance Lean.Lsp.instFileSourceTextDocumentEdit : FileSource TextDocumentEdit

instance Lean.Lsp.instFileSourceTextDocumentItem : FileSource TextDocumentItem

instance Lean.Lsp.instFileSourceTextDocumentPositionParams : FileSource TextDocumentPositionParams

instance Lean.Lsp.instFileSourceDidOpenTextDocumentParams : FileSource DidOpenTextDocumentParams

instance Lean.Lsp.instFileSourceDidChangeTextDocumentParams : FileSource DidChangeTextDocumentParams

instance Lean.Lsp.instFileSourceDidSaveTextDocumentParams : FileSource DidSaveTextDocumentParams

instance Lean.Lsp.instFileSourceDidCloseTextDocumentParams : FileSource DidCloseTextDocumentParams

instance Lean.Lsp.instFileSourceCompletionParams : FileSource CompletionParams

instance Lean.Lsp.instFileSourceHoverParams : FileSource HoverParams

instance Lean.Lsp.instFileSourceDeclarationParams : FileSource DeclarationParams

instance Lean.Lsp.instFileSourceDefinitionParams : FileSource DefinitionParams

instance Lean.Lsp.instFileSourceTypeDefinitionParams : FileSource TypeDefinitionParams

instance Lean.Lsp.instFileSourceReferenceParams : FileSource ReferenceParams

instance Lean.Lsp.instFileSourceWaitForDiagnosticsParams : FileSource WaitForDiagnosticsParams

instance Lean.Lsp.instFileSourceDocumentHighlightParams : FileSource DocumentHighlightParams

instance Lean.Lsp.instFileSourceDocumentSymbolParams : FileSource DocumentSymbolParams

instance Lean.Lsp.instFileSourceSemanticTokensParams : FileSource SemanticTokensParams

instance Lean.Lsp.instFileSourceSemanticTokensRangeParams : FileSource SemanticTokensRangeParams

instance Lean.Lsp.instFileSourceFoldingRangeParams : FileSource FoldingRangeParams

instance Lean.Lsp.instFileSourcePlainGoalParams : FileSource PlainGoalParams

instance Lean.Lsp.instFileSourcePlainTermGoalParams : FileSource PlainTermGoalParams

instance Lean.Lsp.instFileSourceRpcConnectParams : FileSource RpcConnectParams

instance Lean.Lsp.instFileSourceRpcCallParams : FileSource RpcCallParams

instance Lean.Lsp.instFileSourceRpcReleaseParams : FileSource RpcReleaseParams

instance Lean.Lsp.instFileSourceRpcKeepAliveParams : FileSource RpcKeepAliveParams

instance Lean.Lsp.instFileSourceCodeActionParams : FileSource CodeActionParams

instance Lean.Lsp.instFileSourceInlayHintParams : FileSource InlayHintParams