- uri : Lean.Lsp.DocumentUri
- name : String
Equations
Equations
- Lean.Lsp.instFromJsonWorkspaceFolder = { fromJson? := Lean.Lsp.fromJsonWorkspaceFolder✝ }
- globPattern : String
- Created: Lean.Lsp.FileChangeType
- Changed: Lean.Lsp.FileChangeType
- Deleted: Lean.Lsp.FileChangeType
Equations
- One or more equations did not get rendered due to their size.
- uri : Lean.Lsp.DocumentUri
- type : Lean.Lsp.FileChangeType