inductive IO.Error : Type

Exceptions that may be thrown in the IO monad.

Many of the constructors of IO.Error correspond to POSIX error numbers. In these cases, the documentation string lists POSIX standard error macros that correspond to the error. This list is not necessarily exhaustive, and these constructor includes a field for the underlying error number.

• alreadyExists (filename : Option String) (osCode : UInt32) (details : String) : Error

  The operation failed because a file already exists.

  This corresponds to POSIX errors EEXIST, EINPROGRESS, and EISCONN.

• otherError (osCode : UInt32) (details : String) : Error

  Some error not covered by the other constructors of IO.Error occurred.

  This also includes POSIX error EFAULT.

• resourceBusy (osCode : UInt32) (details : String) : Error

  A necessary resource was busy.

  This corresponds to POSIX errors EADDRINUSE, EBUSY, EDEADLK, and ETXTBSY.

• resourceVanished (osCode : UInt32) (details : String) : Error

  A necessary resource is no longer available.

  This corresponds to POSIX errors ECONNRESET, EIDRM, ENETDOWN, ENETRESET, ENOLINK, and EPIPE.

• unsupportedOperation (osCode : UInt32) (details : String) : Error

  An operation was not supported.

  This corresponds to POSIX errors EADDRNOTAVAIL, EAFNOSUPPORT, ENODEV, ENOPROTOOPT ENOSYS, EOPNOTSUPP, ERANGE, ESPIPE, and EXDEV.

• hardwareFault (osCode : UInt32) (details : String) : Error

  The operation failed due to a hardware problem, such as an I/O error.

  This corresponds to the POSIX error EIO.

• unsatisfiedConstraints (osCode : UInt32) (details : String) : Error

  A constraint required by an operation was not satisfied (e.g. a directory was not empty).

  This corresponds to the POSIX error ENOTEMPTY.

• illegalOperation (osCode : UInt32) (details : String) : Error

  An inappropriate I/O control operation was attempted.

  This corresponds to the POSIX error ENOTTY.

• protocolError (osCode : UInt32) (details : String) : Error

  A protocol error occurred.

  This corresponds to the POSIX errors EPROTO, EPROTONOSUPPORT, and EPROTOTYPE.

• timeExpired (osCode : UInt32) (details : String) : Error

  An operation timed out.

  This corresponds to the POSIX errors ETIME, and ETIMEDOUT.

• interrupted (filename : String) (osCode : UInt32) (details : String) : Error

  The operation was interrupted.

  This corresponds to the POSIX error EINTR.

• noFileOrDirectory (filename : String) (osCode : UInt32) (details : String) : Error

  No such file or directory.

  This corresponds to the POSIX error ENOENT.

• invalidArgument (filename : Option String) (osCode : UInt32) (details : String) : Error

  An argument to an I/O operation was invalid.

  This corresponds to the POSIX errors ELOOP, ENAMETOOLONG, EDESTADDRREQ, EILSEQ, EINVAL, EDOM, EBADF ENOEXEC, ENOSTR, ENOTCONN, and ENOTSOCK.

• permissionDenied (filename : Option String) (osCode : UInt32) (details : String) : Error

  An operation failed due to insufficient permissions.

  This corresponds to the POSIX errors EACCES, EROFS, ECONNABORTED, EFBIG, and EPERM.

• resourceExhausted (filename : Option String) (osCode : UInt32) (details : String) : Error

  A resource was exhausted.

  This corresponds to the POSIX errors EMFILE, ENFILE, ENOSPC, E2BIG, EAGAIN, EMLINK, EMSGSIZE, ENOBUFS, ENOLCK, ENOMEM, and ENOSR.

• inappropriateType (filename : Option String) (osCode : UInt32) (details : String) : Error

  An argument was the wrong type (e.g. a directory when a file was required).

  This corresponds to the POSIX errors EISDIR, EBADMSG, and ENOTDIR.

• noSuchThing (filename : Option String) (osCode : UInt32) (details : String) : Error

  A required resource does not exist.

  This corresponds to the POSIX errors ENXIO, EHOSTUNREACH, ENETUNREACH, ECHILD, ECONNREFUSED, ENODATA, ENOMSG, and ESRCH.

• unexpectedEof : Error

  An unexpected end-of-file marker was encountered.

• userError (msg : String) : Error

  Some other error occurred.

instance instInhabitedError : Inhabited IO.Error

Equations

• instInhabitedError = { default := IO.Error.userError "(`Inhabited.default` for `IO.Error`)" }

@[export lean_mk_io_user_error]

def IO.userError (s : String) : Error

Constructs an IO.Error from a string.

IO.Error is the type of exceptions thrown by the IO monad.

Equations

• IO.userError s = IO.Error.userError s

instance instCoeStringError : Coe String IO.Error

Equations

• instCoeStringError = { coe := IO.userError }

@[export lean_mk_io_error_already_exists_file]

def IO.Error.mkAlreadyExistsFile : String → UInt32 → String → Error

Equations

• IO.Error.mkAlreadyExistsFile = IO.Error.alreadyExists ∘ some

@[export lean_mk_io_error_eof]

def IO.Error.mkEofError : Unit → Error

Equations

• IO.Error.mkEofError x✝ = IO.Error.unexpectedEof

@[export lean_mk_io_error_inappropriate_type_file]

def IO.Error.mkInappropriateTypeFile : String → UInt32 → String → Error

Equations

• IO.Error.mkInappropriateTypeFile = IO.Error.inappropriateType ∘ some

@[export lean_mk_io_error_interrupted]

def IO.Error.mkInterrupted : String → UInt32 → String → Error

Equations

• IO.Error.mkInterrupted = IO.Error.interrupted

@[export lean_mk_io_error_invalid_argument_file]

def IO.Error.mkInvalidArgumentFile : String → UInt32 → String → Error

Equations

• IO.Error.mkInvalidArgumentFile = IO.Error.invalidArgument ∘ some

@[export lean_mk_io_error_no_file_or_directory]

def IO.Error.mkNoFileOrDirectory : String → UInt32 → String → Error

Equations

• IO.Error.mkNoFileOrDirectory = IO.Error.noFileOrDirectory

@[export lean_mk_io_error_no_such_thing_file]

def IO.Error.mkNoSuchThingFile : String → UInt32 → String → Error

Equations

• IO.Error.mkNoSuchThingFile = IO.Error.noSuchThing ∘ some

@[export lean_mk_io_error_permission_denied_file]

def IO.Error.mkPermissionDeniedFile : String → UInt32 → String → Error

Equations

• IO.Error.mkPermissionDeniedFile = IO.Error.permissionDenied ∘ some

@[export lean_mk_io_error_resource_exhausted_file]

def IO.Error.mkResourceExhaustedFile : String → UInt32 → String → Error

Equations

• IO.Error.mkResourceExhaustedFile = IO.Error.resourceExhausted ∘ some

@[export lean_mk_io_error_unsupported_operation]

def IO.Error.mkUnsupportedOperation : UInt32 → String → Error

Equations

• IO.Error.mkUnsupportedOperation = IO.Error.unsupportedOperation

@[export lean_mk_io_error_resource_exhausted]

def IO.Error.mkResourceExhausted : UInt32 → String → Error

Equations

• IO.Error.mkResourceExhausted = IO.Error.resourceExhausted none

@[export lean_mk_io_error_already_exists]

def IO.Error.mkAlreadyExists : UInt32 → String → Error

Equations

• IO.Error.mkAlreadyExists = IO.Error.alreadyExists none

@[export lean_mk_io_error_inappropriate_type]

def IO.Error.mkInappropriateType : UInt32 → String → Error

Equations

• IO.Error.mkInappropriateType = IO.Error.inappropriateType none

@[export lean_mk_io_error_no_such_thing]

def IO.Error.mkNoSuchThing : UInt32 → String → Error

Equations

• IO.Error.mkNoSuchThing = IO.Error.noSuchThing none

@[export lean_mk_io_error_resource_vanished]

def IO.Error.mkResourceVanished : UInt32 → String → Error

Equations

• IO.Error.mkResourceVanished = IO.Error.resourceVanished

@[export lean_mk_io_error_resource_busy]

def IO.Error.mkResourceBusy : UInt32 → String → Error

Equations

• IO.Error.mkResourceBusy = IO.Error.resourceBusy

@[export lean_mk_io_error_invalid_argument]

def IO.Error.mkInvalidArgument : UInt32 → String → Error

Equations

• IO.Error.mkInvalidArgument = IO.Error.invalidArgument none

@[export lean_mk_io_error_other_error]

def IO.Error.mkOtherError : UInt32 → String → Error

Equations

• IO.Error.mkOtherError = IO.Error.otherError

@[export lean_mk_io_error_permission_denied]

def IO.Error.mkPermissionDenied : UInt32 → String → Error

Equations

• IO.Error.mkPermissionDenied = IO.Error.permissionDenied none

@[export lean_mk_io_error_hardware_fault]

def IO.Error.mkHardwareFault : UInt32 → String → Error

Equations

• IO.Error.mkHardwareFault = IO.Error.hardwareFault

@[export lean_mk_io_error_unsatisfied_constraints]

def IO.Error.mkUnsatisfiedConstraints : UInt32 → String → Error

Equations

• IO.Error.mkUnsatisfiedConstraints = IO.Error.unsatisfiedConstraints

@[export lean_mk_io_error_illegal_operation]

def IO.Error.mkIllegalOperation : UInt32 → String → Error

Equations

• IO.Error.mkIllegalOperation = IO.Error.illegalOperation

@[export lean_mk_io_error_protocol_error]

def IO.Error.mkProtocolError : UInt32 → String → Error

Equations

• IO.Error.mkProtocolError = IO.Error.protocolError

@[export lean_mk_io_error_time_expired]

def IO.Error.mkTimeExpired : UInt32 → String → Error

Equations

• IO.Error.mkTimeExpired = IO.Error.timeExpired

def IO.Error.fopenErrorToString (gist fn : String) (code : UInt32) : Option String → String

Equations

• One or more equations did not get rendered due to their size.
• IO.Error.fopenErrorToString gist fn code none = IO.Error.downCaseFirst✝ gist ++ " (error code: " ++ toString code ++ ")\n file: " ++ fn

def IO.Error.otherErrorToString (gist : String) (code : UInt32) : Option String → String

Equations

• IO.Error.otherErrorToString gist code (some details) = IO.Error.downCaseFirst✝ gist ++ " (error code: " ++ toString code ++ ", " ++ IO.Error.downCaseFirst✝¹ details ++ ")"
• IO.Error.otherErrorToString gist code none = IO.Error.downCaseFirst✝ gist ++ " (error code: " ++ toString code ++ ")"

@[export lean_io_error_to_string]

def IO.Error.toString : Error → String

Converts an IO.Error to a descriptive string.

IO.Error.userError is converted to its embedded message. The other constructors are converted in a way that preserves structured information, such as error codes and filenames, that can help diagnose the issue.

Equations

• IO.Error.unexpectedEof.toString = "end of file"
• (IO.Error.inappropriateType (some fn) code details).toString = IO.Error.fopenErrorToString "inappropriate type" fn code (some details)
• (IO.Error.inappropriateType none code details).toString = IO.Error.otherErrorToString "inappropriate type" code (some details)
• (IO.Error.interrupted fn code details).toString = IO.Error.fopenErrorToString "interrupted system call" fn code (some details)
• (IO.Error.invalidArgument (some fn) code details).toString = IO.Error.fopenErrorToString "invalid argument" fn code (some details)
• (IO.Error.invalidArgument none code details).toString = IO.Error.otherErrorToString "invalid argument" code (some details)
• (IO.Error.noFileOrDirectory fn code details).toString = IO.Error.fopenErrorToString "no such file or directory" fn code none
• (IO.Error.noSuchThing (some fn) code details).toString = IO.Error.fopenErrorToString "no such thing" fn code (some details)
• (IO.Error.noSuchThing none code details).toString = IO.Error.otherErrorToString "no such thing" code (some details)
• (IO.Error.permissionDenied (some fn) code details).toString = IO.Error.fopenErrorToString details fn code none
• (IO.Error.permissionDenied none code details).toString = IO.Error.otherErrorToString details code none
• (IO.Error.resourceExhausted (some fn) code details).toString = IO.Error.fopenErrorToString "resource exhausted" fn code (some details)
• (IO.Error.resourceExhausted none code details).toString = IO.Error.otherErrorToString "resource exhausted" code (some details)
• (IO.Error.alreadyExists none code details).toString = IO.Error.otherErrorToString "already exists" code (some details)
• (IO.Error.alreadyExists (some fn) code details).toString = IO.Error.fopenErrorToString "already exists" fn code (some details)
• (IO.Error.otherError code details).toString = IO.Error.otherErrorToString details code none
• (IO.Error.resourceBusy code details).toString = IO.Error.otherErrorToString "resource busy" code (some details)
• (IO.Error.resourceVanished code details).toString = IO.Error.otherErrorToString "resource vanished" code (some details)
• (IO.Error.hardwareFault code details).toString = IO.Error.otherErrorToString "hardware fault" code none
• (IO.Error.illegalOperation code details).toString = IO.Error.otherErrorToString "illegal operation" code (some details)
• (IO.Error.protocolError code details).toString = IO.Error.otherErrorToString "protocol error" code (some details)
• (IO.Error.timeExpired code details).toString = IO.Error.otherErrorToString "time expired" code (some details)
• (IO.Error.unsatisfiedConstraints code details).toString = IO.Error.otherErrorToString "directory not empty" code none
• (IO.Error.unsupportedOperation code details).toString = IO.Error.otherErrorToString "unsupported operation" code (some details)
• (IO.Error.userError msg).toString = msg

instance IO.Error.instToString : ToString Error

Equations

• IO.Error.instToString = { toString := IO.Error.toString }