Lean.Server.FileSource

source

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

Type

fileSource : α → Lean.Lsp.DocumentUri

Instances

source

instance Lean.Lsp.instFileSourceLocation:

Lean.Lsp.FileSource Lean.Lsp.Location

Equations

Lean.Lsp.instFileSourceLocation = { fileSource := fun l => l.uri }

source

instance Lean.Lsp.instFileSourceTextDocumentIdentifier:

Lean.Lsp.FileSource Lean.Lsp.TextDocumentIdentifier

Equations

Lean.Lsp.instFileSourceTextDocumentIdentifier = { fileSource := fun i => i.uri }

source

instance Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier:

Lean.Lsp.FileSource Lean.Lsp.VersionedTextDocumentIdentifier

Equations

Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier = { fileSource := fun i => i.uri }

source

instance Lean.Lsp.instFileSourceTextDocumentEdit:

Lean.Lsp.FileSource Lean.Lsp.TextDocumentEdit

Equations

Lean.Lsp.instFileSourceTextDocumentEdit = { fileSource := fun e => Lean.Lsp.fileSource e.textDocument }

source

instance Lean.Lsp.instFileSourceTextDocumentItem:

Lean.Lsp.FileSource Lean.Lsp.TextDocumentItem

Equations

Lean.Lsp.instFileSourceTextDocumentItem = { fileSource := fun i => i.uri }

source

instance Lean.Lsp.instFileSourceTextDocumentPositionParams:

Lean.Lsp.FileSource Lean.Lsp.TextDocumentPositionParams

Equations

Lean.Lsp.instFileSourceTextDocumentPositionParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }

source

instance Lean.Lsp.instFileSourceDidOpenTextDocumentParams:

Lean.Lsp.FileSource Lean.Lsp.DidOpenTextDocumentParams

Equations

Lean.Lsp.instFileSourceDidOpenTextDocumentParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }

source

instance Lean.Lsp.instFileSourceDidChangeTextDocumentParams:

Lean.Lsp.FileSource Lean.Lsp.DidChangeTextDocumentParams

Equations

Lean.Lsp.instFileSourceDidChangeTextDocumentParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }

source

instance Lean.Lsp.instFileSourceDidCloseTextDocumentParams:

Lean.Lsp.FileSource Lean.Lsp.DidCloseTextDocumentParams

Equations

Lean.Lsp.instFileSourceDidCloseTextDocumentParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }

source

instance Lean.Lsp.instFileSourceCompletionParams:

Lean.Lsp.FileSource Lean.Lsp.CompletionParams

Equations

Lean.Lsp.instFileSourceCompletionParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source

instance Lean.Lsp.instFileSourceHoverParams:

Lean.Lsp.FileSource Lean.Lsp.HoverParams

Equations

Lean.Lsp.instFileSourceHoverParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source

instance Lean.Lsp.instFileSourceDeclarationParams:

Lean.Lsp.FileSource Lean.Lsp.DeclarationParams

Equations

Lean.Lsp.instFileSourceDeclarationParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source

instance Lean.Lsp.instFileSourceDefinitionParams:

Lean.Lsp.FileSource Lean.Lsp.DefinitionParams

Equations

Lean.Lsp.instFileSourceDefinitionParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source

instance Lean.Lsp.instFileSourceTypeDefinitionParams:

Lean.Lsp.FileSource Lean.Lsp.TypeDefinitionParams

Equations

Lean.Lsp.instFileSourceTypeDefinitionParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source

instance Lean.Lsp.instFileSourceReferenceParams:

Lean.Lsp.FileSource Lean.Lsp.ReferenceParams

Equations

Lean.Lsp.instFileSourceReferenceParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source

instance Lean.Lsp.instFileSourceWaitForDiagnosticsParams:

Lean.Lsp.FileSource Lean.Lsp.WaitForDiagnosticsParams

Equations

Lean.Lsp.instFileSourceWaitForDiagnosticsParams = { fileSource := fun p => p.uri }

source

instance Lean.Lsp.instFileSourceDocumentHighlightParams:

Lean.Lsp.FileSource Lean.Lsp.DocumentHighlightParams

Equations

Lean.Lsp.instFileSourceDocumentHighlightParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source

instance Lean.Lsp.instFileSourceDocumentSymbolParams:

Lean.Lsp.FileSource Lean.Lsp.DocumentSymbolParams

Equations

Lean.Lsp.instFileSourceDocumentSymbolParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }

source

instance Lean.Lsp.instFileSourceSemanticTokensParams:

Lean.Lsp.FileSource Lean.Lsp.SemanticTokensParams

Equations

Lean.Lsp.instFileSourceSemanticTokensParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }

source

instance Lean.Lsp.instFileSourceSemanticTokensRangeParams:

Lean.Lsp.FileSource Lean.Lsp.SemanticTokensRangeParams

Equations

Lean.Lsp.instFileSourceSemanticTokensRangeParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }

source

instance Lean.Lsp.instFileSourceFoldingRangeParams:

Lean.Lsp.FileSource Lean.Lsp.FoldingRangeParams

Equations

Lean.Lsp.instFileSourceFoldingRangeParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }

source

instance Lean.Lsp.instFileSourcePlainGoalParams:

Lean.Lsp.FileSource Lean.Lsp.PlainGoalParams

Equations

Lean.Lsp.instFileSourcePlainGoalParams = { fileSource := fun p => Lean.Lsp.fileSource p.toTextDocumentPositionParams.textDocument }

source

instance Lean.Lsp.instFileSourcePlainTermGoalParams:

Lean.Lsp.FileSource Lean.Lsp.PlainTermGoalParams

Equations

Lean.Lsp.instFileSourcePlainTermGoalParams = { fileSource := fun p => Lean.Lsp.fileSource p.toTextDocumentPositionParams.textDocument }

source

instance Lean.Lsp.instFileSourceRpcConnectParams:

Lean.Lsp.FileSource Lean.Lsp.RpcConnectParams

Equations

Lean.Lsp.instFileSourceRpcConnectParams = { fileSource := fun p => p.uri }

source

instance Lean.Lsp.instFileSourceRpcCallParams:

Lean.Lsp.FileSource Lean.Lsp.RpcCallParams

Equations

Lean.Lsp.instFileSourceRpcCallParams = { fileSource := fun p => Lean.Lsp.fileSource p.toTextDocumentPositionParams.textDocument }

source

instance Lean.Lsp.instFileSourceRpcReleaseParams:

Lean.Lsp.FileSource Lean.Lsp.RpcReleaseParams

Equations

Lean.Lsp.instFileSourceRpcReleaseParams = { fileSource := fun p => p.uri }

source

instance Lean.Lsp.instFileSourceRpcKeepAliveParams:

Lean.Lsp.FileSource Lean.Lsp.RpcKeepAliveParams

Equations

Lean.Lsp.instFileSourceRpcKeepAliveParams = { fileSource := fun p => p.uri }