Documentation

Init.System.IOError

inductive IO.Error :

Imitate the structure of IOErrorType in Haskell: https://hackage.haskell.org/package/base-4.12.0.0/docs/System-IO-Error.html#t:IOErrorType

Instances For
    Equations
    @[export lean_mk_io_user_error]
    Equations
    Instances For
      @[export lean_mk_io_error_already_exists_file]
      Equations
      Instances For
        @[export lean_mk_io_error_eof]
        Equations
        Instances For
          @[export lean_mk_io_error_inappropriate_type_file]
          Equations
          Instances For
            @[export lean_mk_io_error_interrupted]
            Equations
            Instances For
              @[export lean_mk_io_error_invalid_argument_file]
              Equations
              Instances For
                @[export lean_mk_io_error_no_file_or_directory]
                Equations
                Instances For
                  @[export lean_mk_io_error_no_such_thing_file]
                  Equations
                  Instances For
                    @[export lean_mk_io_error_permission_denied_file]
                    Equations
                    Instances For
                      @[export lean_mk_io_error_resource_exhausted_file]
                      Equations
                      Instances For
                        @[export lean_mk_io_error_unsupported_operation]
                        Equations
                        Instances For
                          @[export lean_mk_io_error_resource_exhausted]
                          Equations
                          Instances For
                            @[export lean_mk_io_error_already_exists]
                            Equations
                            Instances For
                              @[export lean_mk_io_error_inappropriate_type]
                              Equations
                              Instances For
                                @[export lean_mk_io_error_no_such_thing]
                                Equations
                                Instances For
                                  @[export lean_mk_io_error_resource_vanished]
                                  Equations
                                  Instances For
                                    @[export lean_mk_io_error_resource_busy]
                                    Equations
                                    Instances For
                                      @[export lean_mk_io_error_invalid_argument]
                                      Equations
                                      Instances For
                                        @[export lean_mk_io_error_other_error]
                                        Equations
                                        Instances For
                                          @[export lean_mk_io_error_permission_denied]
                                          Equations
                                          Instances For
                                            @[export lean_mk_io_error_hardware_fault]
                                            Equations
                                            Instances For
                                              @[export lean_mk_io_error_unsatisfied_constraints]
                                              Equations
                                              Instances For
                                                @[export lean_mk_io_error_illegal_operation]
                                                Equations
                                                Instances For
                                                  @[export lean_mk_io_error_protocol_error]
                                                  Equations
                                                  Instances For
                                                    @[export lean_mk_io_error_time_expired]
                                                    Equations
                                                    Instances For
                                                      Equations
                                                      Instances For
                                                        Equations
                                                        Instances For
                                                          @[export lean_io_error_to_string]
                                                          Equations
                                                          Instances For