- fileSource : α → Lean.Lsp.DocumentUri
Instances
- Lean.Lsp.instFileSourceDocumentHighlightParams
- Lean.Lsp.instFileSourceCompletionParams
- Lean.Lsp.instFileSourceRpcConnectParams
- Lean.Lsp.instFileSourcePlainGoalParams
- Lean.Lsp.instFileSourceDidCloseTextDocumentParams
- Lean.Lsp.instFileSourceHoverParams
- Lean.Lsp.instFileSourceTextDocumentEdit
- Lean.Lsp.instFileSourcePlainTermGoalParams
- Lean.Lsp.instFileSourceTextDocumentPositionParams
- Lean.Lsp.instFileSourceSemanticTokensParams
- Lean.Lsp.instFileSourceDeclarationParams
- Lean.Lsp.instFileSourceDocumentSymbolParams
- Lean.Lsp.instFileSourceDidChangeTextDocumentParams
- Lean.Lsp.instFileSourceSemanticTokensRangeParams
- Lean.Lsp.instFileSourceReferenceParams
- Lean.Lsp.instFileSourceRpcCallParams
- Lean.Lsp.instFileSourceRpcKeepAliveParams
- Lean.Lsp.instFileSourceTextDocumentIdentifier
- Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier
- Lean.Lsp.instFileSourceWaitForDiagnosticsParams
- Lean.Lsp.instFileSourceLocation
- Lean.Lsp.instFileSourceRpcReleaseParams
- Lean.Lsp.instFileSourceTypeDefinitionParams
- Lean.Lsp.instFileSourceTextDocumentItem
- Lean.Lsp.instFileSourceDefinitionParams
- Lean.Lsp.instFileSourceDidOpenTextDocumentParams
Equations
- Lean.Lsp.instFileSourceLocation = { fileSource := fun l => l.uri }
Equations
- Lean.Lsp.instFileSourceTextDocumentIdentifier = { fileSource := fun i => i.uri }
Equations
- Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier = { fileSource := fun i => i.uri }
Equations
- Lean.Lsp.instFileSourceTextDocumentEdit = { fileSource := fun e => Lean.Lsp.fileSource e.textDocument }
Equations
- Lean.Lsp.instFileSourceTextDocumentItem = { fileSource := fun i => i.uri }
Equations
- Lean.Lsp.instFileSourceTextDocumentPositionParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceDidOpenTextDocumentParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceDidChangeTextDocumentParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceDidCloseTextDocumentParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceCompletionParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceHoverParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceDeclarationParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceDefinitionParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceTypeDefinitionParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceReferenceParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceWaitForDiagnosticsParams = { fileSource := fun p => p.uri }
Equations
- Lean.Lsp.instFileSourceDocumentHighlightParams = { fileSource := fun h => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceDocumentSymbolParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceSemanticTokensParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceSemanticTokensRangeParams = { fileSource := fun p => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourcePlainGoalParams = { fileSource := fun p => Lean.Lsp.fileSource p.toTextDocumentPositionParams.textDocument }
Equations
- Lean.Lsp.instFileSourcePlainTermGoalParams = { fileSource := fun p => Lean.Lsp.fileSource p.toTextDocumentPositionParams.textDocument }
Equations
- Lean.Lsp.instFileSourceRpcConnectParams = { fileSource := fun p => p.uri }
Equations
- Lean.Lsp.instFileSourceRpcCallParams = { fileSource := fun p => Lean.Lsp.fileSource p.toTextDocumentPositionParams.textDocument }
Equations
- Lean.Lsp.instFileSourceRpcReleaseParams = { fileSource := fun p => p.uri }
Equations
- Lean.Lsp.instFileSourceRpcKeepAliveParams = { fileSource := fun p => p.uri }