Init.System.IOError

inductive IO.Error :

alreadyExists: Option String → UInt32 → String → IO.Error
otherError: UInt32 → String → IO.Error
resourceBusy: UInt32 → String → IO.Error
resourceVanished: UInt32 → String → IO.Error
unsupportedOperation: UInt32 → String → IO.Error
hardwareFault: UInt32 → String → IO.Error
unsatisfiedConstraints: UInt32 → String → IO.Error
illegalOperation: UInt32 → String → IO.Error
protocolError: UInt32 → String → IO.Error
timeExpired: UInt32 → String → IO.Error
interrupted: String → UInt32 → String → IO.Error
noFileOrDirectory: String → UInt32 → String → IO.Error
invalidArgument: Option String → UInt32 → String → IO.Error
permissionDenied: Option String → UInt32 → String → IO.Error
resourceExhausted: Option String → UInt32 → String → IO.Error
inappropriateType: Option String → UInt32 → String → IO.Error
noSuchThing: Option String → UInt32 → String → IO.Error
unexpectedEof: IO.Error
userError: String → 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

source

instance IO.instInhabitedError :

Inhabited IO.Error

source

@[export lean_mk_io_user_error]

def IO.userError (s : String) :

IO.Error

Instances For

source

instance instCoeStringError :

Coe String IO.Error

source

@[export lean_mk_io_error_already_exists_file]

def IO.Error.mkAlreadyExistsFile :

String → UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_eof]

def IO.Error.mkEofError :

Unit → IO.Error

Instances For

source

@[export lean_mk_io_error_inappropriate_type_file]

def IO.Error.mkInappropriateTypeFile :

String → UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_interrupted]

def IO.Error.mkInterrupted :

String → UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_invalid_argument_file]

def IO.Error.mkInvalidArgumentFile :

String → UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_no_file_or_directory]

def IO.Error.mkNoFileOrDirectory :

String → UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_no_such_thing_file]

def IO.Error.mkNoSuchThingFile :

String → UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_permission_denied_file]

def IO.Error.mkPermissionDeniedFile :

String → UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_resource_exhausted_file]

def IO.Error.mkResourceExhaustedFile :

String → UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_unsupported_operation]

def IO.Error.mkUnsupportedOperation :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_resource_exhausted]

def IO.Error.mkResourceExhausted :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_already_exists]

def IO.Error.mkAlreadyExists :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_inappropriate_type]

def IO.Error.mkInappropriateType :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_no_such_thing]

def IO.Error.mkNoSuchThing :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_resource_vanished]

def IO.Error.mkResourceVanished :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_resource_busy]

def IO.Error.mkResourceBusy :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_invalid_argument]

def IO.Error.mkInvalidArgument :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_other_error]

def IO.Error.mkOtherError :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_permission_denied]

def IO.Error.mkPermissionDenied :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_hardware_fault]

def IO.Error.mkHardwareFault :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_unsatisfied_constraints]

def IO.Error.mkUnsatisfiedConstraints :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_illegal_operation]

def IO.Error.mkIllegalOperation :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_protocol_error]

def IO.Error.mkProtocolError :

UInt32 → String → IO.Error

Instances For

source

@[export lean_mk_io_error_time_expired]

def IO.Error.mkTimeExpired :

UInt32 → String → IO.Error

Instances For

source

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

Option String → String

Instances For

source

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

Option String → String

Instances For

source

@[export lean_io_error_to_string]

def IO.Error.toString :

IO.Error → String

Instances For

source

instance IO.Error.instToStringError :

ToString IO.Error