structure Lean.Lsp.WorkspaceFolder : Type

• uri : Lean.Lsp.DocumentUri
• name : String

instance Lean.Lsp.instToJsonWorkspaceFolder : Lean.ToJson Lean.Lsp.WorkspaceFolder

Equations

• Lean.Lsp.instToJsonWorkspaceFolder = { toJson := Lean.Lsp.toJsonWorkspaceFolder✝ }

instance Lean.Lsp.instFromJsonWorkspaceFolder : Lean.FromJson Lean.Lsp.WorkspaceFolder

Equations

• Lean.Lsp.instFromJsonWorkspaceFolder = { fromJson? := Lean.Lsp.fromJsonWorkspaceFolder✝ }

structure Lean.Lsp.FileSystemWatcher : Type

• globPattern : String
• kind : Option Nat

instance Lean.Lsp.instFromJsonFileSystemWatcher : Lean.FromJson Lean.Lsp.FileSystemWatcher

Equations

• Lean.Lsp.instFromJsonFileSystemWatcher = { fromJson? := Lean.Lsp.fromJsonFileSystemWatcher✝ }

instance Lean.Lsp.instToJsonFileSystemWatcher : Lean.ToJson Lean.Lsp.FileSystemWatcher

Equations

• Lean.Lsp.instToJsonFileSystemWatcher = { toJson := Lean.Lsp.toJsonFileSystemWatcher✝ }

def Lean.Lsp.FileSystemWatcher.create : Nat

Equations

• Lean.Lsp.FileSystemWatcher.create = 1

def Lean.Lsp.FileSystemWatcher.change : Nat

Equations

• Lean.Lsp.FileSystemWatcher.change = 2

def Lean.Lsp.FileSystemWatcher.delete : Nat

Equations

• Lean.Lsp.FileSystemWatcher.delete = 4

structure Lean.Lsp.DidChangeWatchedFilesRegistrationOptions : Type

• watchers : Array Lean.Lsp.FileSystemWatcher

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions : Lean.FromJson Lean.Lsp.DidChangeWatchedFilesRegistrationOptions

Equations

• Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions = { fromJson? := Lean.Lsp.fromJsonDidChangeWatchedFilesRegistrationOptions✝ }

instance Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions : Lean.ToJson Lean.Lsp.DidChangeWatchedFilesRegistrationOptions

Equations

• Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions = { toJson := Lean.Lsp.toJsonDidChangeWatchedFilesRegistrationOptions✝ }

inductive Lean.Lsp.FileChangeType : Type

• Created : Lean.Lsp.FileChangeType
• Changed : Lean.Lsp.FileChangeType
• Deleted : Lean.Lsp.FileChangeType

instance Lean.Lsp.instFromJsonFileChangeType : Lean.FromJson Lean.Lsp.FileChangeType

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Lsp.instToJsonFileChangeType : Lean.ToJson Lean.Lsp.FileChangeType

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Lsp.FileEvent : Type

• uri : Lean.Lsp.DocumentUri
• type : Lean.Lsp.FileChangeType

instance Lean.Lsp.instFromJsonFileEvent : Lean.FromJson Lean.Lsp.FileEvent

Equations

• Lean.Lsp.instFromJsonFileEvent = { fromJson? := Lean.Lsp.fromJsonFileEvent✝ }

instance Lean.Lsp.instToJsonFileEvent : Lean.ToJson Lean.Lsp.FileEvent

Equations

• Lean.Lsp.instToJsonFileEvent = { toJson := Lean.Lsp.toJsonFileEvent✝ }

structure Lean.Lsp.DidChangeWatchedFilesParams : Type

• changes : Array Lean.Lsp.FileEvent

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesParams : Lean.FromJson Lean.Lsp.DidChangeWatchedFilesParams

Equations

• Lean.Lsp.instFromJsonDidChangeWatchedFilesParams = { fromJson? := Lean.Lsp.fromJsonDidChangeWatchedFilesParams✝ }

instance Lean.Lsp.instToJsonDidChangeWatchedFilesParams : Lean.ToJson Lean.Lsp.DidChangeWatchedFilesParams

Equations

• Lean.Lsp.instToJsonDidChangeWatchedFilesParams = { toJson := Lean.Lsp.toJsonDidChangeWatchedFilesParams✝ }