structure Lean.Lsp.WorkspaceFolder : Type

• uri : DocumentUri
• name : String

Instances For

• Lean.Lsp.instFromJsonWorkspaceFolder
• Lean.Lsp.instToJsonWorkspaceFolder

instance Lean.Lsp.instToJsonWorkspaceFolder : ToJson WorkspaceFolder

Equations

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

instance Lean.Lsp.instFromJsonWorkspaceFolder : FromJson WorkspaceFolder

Equations

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

structure Lean.Lsp.FileSystemWatcher : Type

• globPattern : String
• kind : Option Nat

Instances For

• Lean.Lsp.instFromJsonFileSystemWatcher
• Lean.Lsp.instToJsonFileSystemWatcher

instance Lean.Lsp.instFromJsonFileSystemWatcher : FromJson FileSystemWatcher

Equations

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

instance Lean.Lsp.instToJsonFileSystemWatcher : ToJson 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 FileSystemWatcher

Instances For

• Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions
• Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions : FromJson DidChangeWatchedFilesRegistrationOptions

Equations

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

instance Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions : ToJson DidChangeWatchedFilesRegistrationOptions

Equations

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

inductive Lean.Lsp.FileChangeType : Type

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

Instances For

• Lean.Lsp.instFromJsonFileChangeType
• Lean.Lsp.instToJsonFileChangeType

instance Lean.Lsp.instFromJsonFileChangeType : FromJson FileChangeType

Equations

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

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

Instances For

• Lean.Lsp.instFromJsonFileEvent
• Lean.Lsp.instToJsonFileEvent

instance Lean.Lsp.instFromJsonFileEvent : FromJson FileEvent

Equations

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

instance Lean.Lsp.instToJsonFileEvent : ToJson FileEvent

Equations

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

structure Lean.Lsp.DidChangeWatchedFilesParams : Type

• changes : Array FileEvent

Instances For

• Lean.Lsp.instFromJsonDidChangeWatchedFilesParams
• Lean.Lsp.instToJsonDidChangeWatchedFilesParams

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesParams : FromJson DidChangeWatchedFilesParams

Equations

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

instance Lean.Lsp.instToJsonDidChangeWatchedFilesParams : ToJson DidChangeWatchedFilesParams

Equations

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