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

• fileSource : α → Lean.Lsp.DocumentUri

instance Lean.Lsp.instFileSourceLocation : Lean.Lsp.FileSource Lean.Lsp.Location

instance Lean.Lsp.instFileSourceTextDocumentIdentifier : Lean.Lsp.FileSource Lean.Lsp.TextDocumentIdentifier

instance Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier : Lean.Lsp.FileSource Lean.Lsp.VersionedTextDocumentIdentifier

Equations

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

instance Lean.Lsp.instFileSourceTextDocumentEdit : Lean.Lsp.FileSource Lean.Lsp.TextDocumentEdit

Equations

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

instance Lean.Lsp.instFileSourceTextDocumentItem : Lean.Lsp.FileSource Lean.Lsp.TextDocumentItem

Equations

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

instance Lean.Lsp.instFileSourceTextDocumentPositionParams : Lean.Lsp.FileSource Lean.Lsp.TextDocumentPositionParams

Equations

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

instance Lean.Lsp.instFileSourceDidOpenTextDocumentParams : Lean.Lsp.FileSource Lean.Lsp.DidOpenTextDocumentParams

Equations

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

instance Lean.Lsp.instFileSourceDidChangeTextDocumentParams : Lean.Lsp.FileSource Lean.Lsp.DidChangeTextDocumentParams

Equations

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

instance Lean.Lsp.instFileSourceDidSaveTextDocumentParams : Lean.Lsp.FileSource Lean.Lsp.DidSaveTextDocumentParams

instance Lean.Lsp.instFileSourceDidCloseTextDocumentParams : Lean.Lsp.FileSource Lean.Lsp.DidCloseTextDocumentParams

Equations

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

instance Lean.Lsp.instFileSourceCompletionParams : Lean.Lsp.FileSource Lean.Lsp.CompletionParams

Equations

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

instance Lean.Lsp.instFileSourceHoverParams : Lean.Lsp.FileSource Lean.Lsp.HoverParams

instance Lean.Lsp.instFileSourceDeclarationParams : Lean.Lsp.FileSource Lean.Lsp.DeclarationParams

instance Lean.Lsp.instFileSourceDefinitionParams : Lean.Lsp.FileSource Lean.Lsp.DefinitionParams

instance Lean.Lsp.instFileSourceTypeDefinitionParams : Lean.Lsp.FileSource Lean.Lsp.TypeDefinitionParams

instance Lean.Lsp.instFileSourceReferenceParams : Lean.Lsp.FileSource Lean.Lsp.ReferenceParams

Equations

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

instance Lean.Lsp.instFileSourceWaitForDiagnosticsParams : Lean.Lsp.FileSource Lean.Lsp.WaitForDiagnosticsParams

Equations

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

instance Lean.Lsp.instFileSourceDocumentHighlightParams : Lean.Lsp.FileSource Lean.Lsp.DocumentHighlightParams

instance Lean.Lsp.instFileSourceDocumentSymbolParams : Lean.Lsp.FileSource Lean.Lsp.DocumentSymbolParams

instance Lean.Lsp.instFileSourceSemanticTokensParams : Lean.Lsp.FileSource Lean.Lsp.SemanticTokensParams

Equations

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

instance Lean.Lsp.instFileSourceSemanticTokensRangeParams : Lean.Lsp.FileSource Lean.Lsp.SemanticTokensRangeParams

Equations

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

instance Lean.Lsp.instFileSourceFoldingRangeParams : Lean.Lsp.FileSource Lean.Lsp.FoldingRangeParams

Equations

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

instance Lean.Lsp.instFileSourcePlainGoalParams : Lean.Lsp.FileSource Lean.Lsp.PlainGoalParams

Equations

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

instance Lean.Lsp.instFileSourcePlainTermGoalParams : Lean.Lsp.FileSource Lean.Lsp.PlainTermGoalParams

Equations

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

instance Lean.Lsp.instFileSourceRpcConnectParams : Lean.Lsp.FileSource Lean.Lsp.RpcConnectParams

instance Lean.Lsp.instFileSourceRpcCallParams : Lean.Lsp.FileSource Lean.Lsp.RpcCallParams

instance Lean.Lsp.instFileSourceRpcReleaseParams : Lean.Lsp.FileSource Lean.Lsp.RpcReleaseParams

Equations

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

instance Lean.Lsp.instFileSourceRpcKeepAliveParams : Lean.Lsp.FileSource Lean.Lsp.RpcKeepAliveParams

Equations

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

instance Lean.Lsp.instFileSourceCodeActionParams : Lean.Lsp.FileSource Lean.Lsp.CodeActionParams