inductive IO.Error : Type

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

• 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

instance IO.instInhabitedError : Inhabited IO.Error

Equations

• IO.instInhabitedError = { default := IO.Error.alreadyExists default default default }

@[export lean_mk_io_user_error]

def IO.userError (s : String) : IO.Error

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 → IO.Error

Equations

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

@[export lean_mk_io_error_eof]

def IO.Error.mkEofError : Unit → IO.Error

@[export lean_mk_io_error_inappropriate_type_file]

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

Equations

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

@[export lean_mk_io_error_interrupted]

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

@[export lean_mk_io_error_invalid_argument_file]

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

@[export lean_mk_io_error_no_file_or_directory]

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

@[export lean_mk_io_error_no_such_thing_file]

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

Equations

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

@[export lean_mk_io_error_permission_denied_file]

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

Equations

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

@[export lean_mk_io_error_resource_exhausted_file]

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

@[export lean_mk_io_error_unsupported_operation]

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

@[export lean_mk_io_error_resource_exhausted]

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

Equations

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

@[export lean_mk_io_error_already_exists]

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

Equations

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

@[export lean_mk_io_error_inappropriate_type]

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

Equations

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

@[export lean_mk_io_error_no_such_thing]

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

Equations

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

@[export lean_mk_io_error_resource_vanished]

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

Equations

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

@[export lean_mk_io_error_resource_busy]

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

@[export lean_mk_io_error_invalid_argument]

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

@[export lean_mk_io_error_other_error]

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

@[export lean_mk_io_error_permission_denied]

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

Equations

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

@[export lean_mk_io_error_hardware_fault]

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

@[export lean_mk_io_error_unsatisfied_constraints]

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

@[export lean_mk_io_error_illegal_operation]

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

Equations

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

@[export lean_mk_io_error_protocol_error]

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

Equations

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

@[export lean_mk_io_error_time_expired]

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

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

@[export lean_io_error_to_string]

def IO.Error.toString : IO.Error → String

instance IO.Error.instToString : ToString IO.Error

Equations

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