Documentation

Lean.Data.Lsp.Workspace

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 := [anonymous] }

instance Lean.Lsp.instFromJsonWorkspaceFolder:

Lean.FromJson Lean.Lsp.WorkspaceFolder

Equations

Lean.Lsp.instFromJsonWorkspaceFolder = { fromJson? := [anonymous] }

structure Lean.Lsp.FileSystemWatcher:

Type

globPattern : String
kind : Option Nat

instance Lean.Lsp.instFromJsonFileSystemWatcher:

Lean.FromJson Lean.Lsp.FileSystemWatcher

Equations

Lean.Lsp.instFromJsonFileSystemWatcher = { fromJson? := [anonymous] }

instance Lean.Lsp.instToJsonFileSystemWatcher:

Lean.ToJson Lean.Lsp.FileSystemWatcher

Equations

Lean.Lsp.instToJsonFileSystemWatcher = { toJson := [anonymous] }

def Lean.Lsp.FileSystemWatcher.create:

Equations

Lean.Lsp.FileSystemWatcher.create = 1

def Lean.Lsp.FileSystemWatcher.change:

Equations

Lean.Lsp.FileSystemWatcher.change = 2

def Lean.Lsp.FileSystemWatcher.delete:

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? := [anonymous] }

instance Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions:

Lean.ToJson Lean.Lsp.DidChangeWatchedFilesRegistrationOptions

Equations

Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions = { toJson := [anonymous] }

inductive Lean.Lsp.FileChangeType:

Type

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? := [anonymous] }

instance Lean.Lsp.instToJsonFileEvent:

Lean.ToJson Lean.Lsp.FileEvent

Equations

Lean.Lsp.instToJsonFileEvent = { toJson := [anonymous] }

structure Lean.Lsp.DidChangeWatchedFilesParams:

Type

changes : Array Lean.Lsp.FileEvent

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesParams:

Lean.FromJson Lean.Lsp.DidChangeWatchedFilesParams

Equations

Lean.Lsp.instFromJsonDidChangeWatchedFilesParams = { fromJson? := [anonymous] }

instance Lean.Lsp.instToJsonDidChangeWatchedFilesParams:

Lean.ToJson Lean.Lsp.DidChangeWatchedFilesParams

Equations

Lean.Lsp.instToJsonDidChangeWatchedFilesParams = { toJson := [anonymous] }