Documentation

Lean.Data.Lsp.Workspace

source
structure Lean.Lsp.WorkspaceFolder :
Type
Instances For
    source
    @[instance_reducible]
    instance Lean.Lsp.instToJsonWorkspaceFolder :
    ToJson WorkspaceFolder
    source
    def Lean.Lsp.instToJsonWorkspaceFolder.toJson :
    WorkspaceFolder → Json
    Instances For
      source
      @[instance_reducible]
      instance Lean.Lsp.instFromJsonWorkspaceFolder :
      FromJson WorkspaceFolder
      source
      def Lean.Lsp.instFromJsonWorkspaceFolder.fromJson :
      Json → Except String WorkspaceFolder
      Instances For
        source
        structure Lean.Lsp.FileSystemWatcher :
        Type
        Instances For
          source
          def Lean.Lsp.instFromJsonFileSystemWatcher.fromJson :
          Json → Except String FileSystemWatcher
          Instances For
            source
            @[instance_reducible]
            instance Lean.Lsp.instFromJsonFileSystemWatcher :
            FromJson FileSystemWatcher
            source
            def Lean.Lsp.instToJsonFileSystemWatcher.toJson :
            FileSystemWatcher → Json
            Instances For
              source
              @[instance_reducible]
              instance Lean.Lsp.instToJsonFileSystemWatcher :
              ToJson FileSystemWatcher
              source
              def Lean.Lsp.FileSystemWatcher.create :
              Nat
              Instances For
                source
                def Lean.Lsp.FileSystemWatcher.change :
                Nat
                Instances For
                  source
                  def Lean.Lsp.FileSystemWatcher.delete :
                  Nat
                  Instances For
                    source
                    structure Lean.Lsp.DidChangeWatchedFilesRegistrationOptions :
                    Type
                    Instances For
                      source
                      @[instance_reducible]
                      instance Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions :
                      FromJson DidChangeWatchedFilesRegistrationOptions
                      source
                      def Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions.fromJson :
                      Json → Except String DidChangeWatchedFilesRegistrationOptions
                      Instances For
                        source
                        def Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions.toJson :
                        DidChangeWatchedFilesRegistrationOptions → Json
                        Instances For
                          source
                          @[instance_reducible]
                          instance Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions :
                          ToJson DidChangeWatchedFilesRegistrationOptions
                          source
                          inductive Lean.Lsp.FileChangeType :
                          Type
                          Instances For
                            source
                            @[instance_reducible]
                            instance Lean.Lsp.instFromJsonFileChangeType :
                            FromJson FileChangeType
                            source
                            @[instance_reducible]
                            instance Lean.Lsp.instToJsonFileChangeType :
                            ToJson FileChangeType
                            source
                            structure Lean.Lsp.FileEvent :
                            Type
                            Instances For
                              source
                              @[instance_reducible]
                              instance Lean.Lsp.instFromJsonFileEvent :
                              FromJson FileEvent
                              source
                              def Lean.Lsp.instFromJsonFileEvent.fromJson :
                              Json → Except String FileEvent
                              Instances For
                                source
                                @[instance_reducible]
                                instance Lean.Lsp.instToJsonFileEvent :
                                ToJson FileEvent
                                source
                                def Lean.Lsp.instToJsonFileEvent.toJson :
                                FileEvent → Json
                                Instances For
                                  source
                                  structure Lean.Lsp.DidChangeWatchedFilesParams :
                                  Type
                                  Instances For
                                    source
                                    @[instance_reducible]
                                    instance Lean.Lsp.instFromJsonDidChangeWatchedFilesParams :
                                    FromJson DidChangeWatchedFilesParams
                                    source
                                    def Lean.Lsp.instFromJsonDidChangeWatchedFilesParams.fromJson :
                                    Json → Except String DidChangeWatchedFilesParams
                                    Instances For
                                      source
                                      @[instance_reducible]
                                      instance Lean.Lsp.instToJsonDidChangeWatchedFilesParams :
                                      ToJson DidChangeWatchedFilesParams
                                      source
                                      def Lean.Lsp.instToJsonDidChangeWatchedFilesParams.toJson :
                                      DidChangeWatchedFilesParams → Json
                                      Instances For