Documentation

Lean.Data.Lsp.Workspace

source
structure Lean.Lsp.WorkspaceFolder :
Type
Instances For
    source
    instance Lean.Lsp.instToJsonWorkspaceFolder :
    ToJson WorkspaceFolder
    Equations
      source
      instance Lean.Lsp.instFromJsonWorkspaceFolder :
      FromJson WorkspaceFolder
      Equations
        source
        structure Lean.Lsp.FileSystemWatcher :
        Type
        Instances For
          source
          instance Lean.Lsp.instFromJsonFileSystemWatcher :
          FromJson FileSystemWatcher
          Equations
            source
            instance Lean.Lsp.instToJsonFileSystemWatcher :
            ToJson FileSystemWatcher
            Equations
              source
              def Lean.Lsp.FileSystemWatcher.create :
              Nat
              Equations
                Instances For
                  source
                  def Lean.Lsp.FileSystemWatcher.change :
                  Nat
                  Equations
                    Instances For
                      source
                      def Lean.Lsp.FileSystemWatcher.delete :
                      Nat
                      Equations
                        Instances For
                          source
                          structure Lean.Lsp.DidChangeWatchedFilesRegistrationOptions :
                          Type
                          Instances For
                            source
                            instance Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions :
                            FromJson DidChangeWatchedFilesRegistrationOptions
                            Equations
                              source
                              instance Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions :
                              ToJson DidChangeWatchedFilesRegistrationOptions
                              Equations
                                source
                                inductive Lean.Lsp.FileChangeType :
                                Type
                                Instances For
                                  source
                                  instance Lean.Lsp.instFromJsonFileChangeType :
                                  FromJson FileChangeType
                                  Equations
                                    source
                                    instance Lean.Lsp.instToJsonFileChangeType :
                                    ToJson FileChangeType
                                    Equations
                                      source
                                      structure Lean.Lsp.FileEvent :
                                      Type
                                      Instances For
                                        source
                                        instance Lean.Lsp.instFromJsonFileEvent :
                                        FromJson FileEvent
                                        Equations
                                          source
                                          instance Lean.Lsp.instToJsonFileEvent :
                                          ToJson FileEvent
                                          Equations
                                            source
                                            structure Lean.Lsp.DidChangeWatchedFilesParams :
                                            Type
                                            Instances For
                                              source
                                              instance Lean.Lsp.instFromJsonDidChangeWatchedFilesParams :
                                              FromJson DidChangeWatchedFilesParams
                                              Equations
                                                source
                                                instance Lean.Lsp.instToJsonDidChangeWatchedFilesParams :
                                                ToJson DidChangeWatchedFilesParams
                                                Equations