Documentation

Lean.Server.FileSource

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

fileSource : α → DocumentUri

Instances

instance Lean.Lsp.instFileSourceLocation :

FileSource Location

Equations

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

instance Lean.Lsp.instFileSourceTextDocumentIdentifier :

FileSource TextDocumentIdentifier

Equations

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

instance Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier :

FileSource VersionedTextDocumentIdentifier

Equations

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

instance Lean.Lsp.instFileSourceTextDocumentEdit :

FileSource TextDocumentEdit

Equations

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

instance Lean.Lsp.instFileSourceTextDocumentItem :

FileSource TextDocumentItem

Equations

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

instance Lean.Lsp.instFileSourceTextDocumentPositionParams :

FileSource TextDocumentPositionParams

Equations

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

instance Lean.Lsp.instFileSourceDidOpenTextDocumentParams :

FileSource DidOpenTextDocumentParams

Equations

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

instance Lean.Lsp.instFileSourceDidChangeTextDocumentParams :

FileSource DidChangeTextDocumentParams

Equations

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

instance Lean.Lsp.instFileSourceDidSaveTextDocumentParams :

FileSource DidSaveTextDocumentParams

Equations

Lean.Lsp.instFileSourceDidSaveTextDocumentParams = { fileSource := fun (p : Lean.Lsp.DidSaveTextDocumentParams) => Lean.Lsp.fileSource p.textDocument }

instance Lean.Lsp.instFileSourceDidCloseTextDocumentParams :

FileSource DidCloseTextDocumentParams

Equations

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

instance Lean.Lsp.instFileSourceCompletionParams :

FileSource CompletionParams

Equations

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

instance Lean.Lsp.instFileSourceHoverParams :

FileSource HoverParams

Equations

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

instance Lean.Lsp.instFileSourceDeclarationParams :

FileSource DeclarationParams

Equations

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

instance Lean.Lsp.instFileSourceDefinitionParams :

FileSource DefinitionParams

Equations

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

instance Lean.Lsp.instFileSourceTypeDefinitionParams :

FileSource TypeDefinitionParams

Equations

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

instance Lean.Lsp.instFileSourceReferenceParams :

FileSource ReferenceParams

Equations

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

instance Lean.Lsp.instFileSourceWaitForDiagnosticsParams :

FileSource WaitForDiagnosticsParams

Equations

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

instance Lean.Lsp.instFileSourceDocumentHighlightParams :

FileSource DocumentHighlightParams

Equations

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

instance Lean.Lsp.instFileSourceDocumentSymbolParams :

FileSource DocumentSymbolParams

Equations

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

instance Lean.Lsp.instFileSourceSemanticTokensParams :

FileSource SemanticTokensParams

Equations

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

instance Lean.Lsp.instFileSourceSemanticTokensRangeParams :

FileSource SemanticTokensRangeParams

Equations

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

instance Lean.Lsp.instFileSourceFoldingRangeParams :

FileSource FoldingRangeParams

Equations

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

instance Lean.Lsp.instFileSourcePlainGoalParams :

FileSource PlainGoalParams

Equations

Lean.Lsp.instFileSourcePlainGoalParams = { fileSource := fun (p : Lean.Lsp.PlainGoalParams) => Lean.Lsp.fileSource p.textDocument }

instance Lean.Lsp.instFileSourcePlainTermGoalParams :

FileSource PlainTermGoalParams

Equations

Lean.Lsp.instFileSourcePlainTermGoalParams = { fileSource := fun (p : Lean.Lsp.PlainTermGoalParams) => Lean.Lsp.fileSource p.textDocument }

instance Lean.Lsp.instFileSourceRpcConnectParams :

FileSource RpcConnectParams

Equations

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

instance Lean.Lsp.instFileSourceRpcCallParams :

FileSource RpcCallParams

Equations

Lean.Lsp.instFileSourceRpcCallParams = { fileSource := fun (p : Lean.Lsp.RpcCallParams) => Lean.Lsp.fileSource p.textDocument }

instance Lean.Lsp.instFileSourceRpcReleaseParams :

FileSource RpcReleaseParams

Equations

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

instance Lean.Lsp.instFileSourceRpcKeepAliveParams :

FileSource RpcKeepAliveParams

Equations

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

instance Lean.Lsp.instFileSourceCodeActionParams :

FileSource CodeActionParams

Equations

Lean.Lsp.instFileSourceCodeActionParams = { fileSource := fun (p : Lean.Lsp.CodeActionParams) => Lean.Lsp.fileSource p.textDocument }

instance Lean.Lsp.instFileSourceInlayHintParams :

FileSource InlayHintParams

Equations

Lean.Lsp.instFileSourceInlayHintParams = { fileSource := fun (p : Lean.Lsp.InlayHintParams) => Lean.Lsp.fileSource p.textDocument }

instance Lean.Lsp.instFileSourceSignatureHelpParams :

FileSource SignatureHelpParams

Equations

Lean.Lsp.instFileSourceSignatureHelpParams = { fileSource := fun (p : Lean.Lsp.SignatureHelpParams) => Lean.Lsp.fileSource p.textDocument }