structure Lean.Lsp.WorkspaceFolder : Type

• uri : DocumentUri
• name : String

@[implicit_reducible]

instance Lean.Lsp.instToJsonWorkspaceFolder : ToJson WorkspaceFolder

Equations

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

def Lean.Lsp.instToJsonWorkspaceFolder.toJson : WorkspaceFolder → Json

Equations

• Lean.Lsp.instToJsonWorkspaceFolder.toJson x✝ = Lean.Json.mkObj [[("uri", Lean.toJson x✝.uri)], [("name", Lean.toJson x✝.name)]].flatten

@[implicit_reducible]

instance Lean.Lsp.instFromJsonWorkspaceFolder : FromJson WorkspaceFolder

Equations

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

def Lean.Lsp.instFromJsonWorkspaceFolder.fromJson : Json → Except String WorkspaceFolder

Equations

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

structure Lean.Lsp.FileSystemWatcher : Type

• globPattern : String
• kind? : Option Nat

def Lean.Lsp.instFromJsonFileSystemWatcher.fromJson : Json → Except String FileSystemWatcher

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonFileSystemWatcher : FromJson FileSystemWatcher

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonFileSystemWatcher : ToJson FileSystemWatcher

Equations

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

def Lean.Lsp.instToJsonFileSystemWatcher.toJson : FileSystemWatcher → Json

Equations

• Lean.Lsp.instToJsonFileSystemWatcher.toJson x✝ = Lean.Json.mkObj [[("globPattern", Lean.toJson x✝.globPattern)], Lean.Json.opt "kind" x✝.kind?].flatten

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 FileSystemWatcher

def Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions.fromJson : Json → Except String DidChangeWatchedFilesRegistrationOptions

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions : FromJson DidChangeWatchedFilesRegistrationOptions

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions : ToJson DidChangeWatchedFilesRegistrationOptions

Equations

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

def Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions.toJson : DidChangeWatchedFilesRegistrationOptions → Json

Equations

• Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions.toJson x✝ = Lean.Json.mkObj [[("watchers", Lean.toJson x✝.watchers)]].flatten

inductive Lean.Lsp.FileChangeType : Type

• Created : FileChangeType
• Changed : FileChangeType
• Deleted : FileChangeType

@[implicit_reducible]

instance Lean.Lsp.instFromJsonFileChangeType : FromJson FileChangeType

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonFileChangeType : ToJson FileChangeType

Equations

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

structure Lean.Lsp.FileEvent : Type

• uri : DocumentUri
• type : FileChangeType

def Lean.Lsp.instFromJsonFileEvent.fromJson : Json → Except String FileEvent

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonFileEvent : FromJson FileEvent

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonFileEvent : ToJson FileEvent

Equations

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

def Lean.Lsp.instToJsonFileEvent.toJson : FileEvent → Json

Equations

• Lean.Lsp.instToJsonFileEvent.toJson x✝ = Lean.Json.mkObj [[("uri", Lean.toJson x✝.uri)], [("type", Lean.toJson x✝.type)]].flatten

structure Lean.Lsp.DidChangeWatchedFilesParams : Type

• changes : Array FileEvent

def Lean.Lsp.instFromJsonDidChangeWatchedFilesParams.fromJson : Json → Except String DidChangeWatchedFilesParams

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesParams : FromJson DidChangeWatchedFilesParams

Equations

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

def Lean.Lsp.instToJsonDidChangeWatchedFilesParams.toJson : DidChangeWatchedFilesParams → Json

Equations

• Lean.Lsp.instToJsonDidChangeWatchedFilesParams.toJson x✝ = Lean.Json.mkObj [[("changes", Lean.toJson x✝.changes)]].flatten

@[implicit_reducible]

instance Lean.Lsp.instToJsonDidChangeWatchedFilesParams : ToJson DidChangeWatchedFilesParams

Equations

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