inductive IO.Error : Type

• 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

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

Equations

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

@[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

Equations

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

@[export lean_mk_io_error_invalid_argument_file]

def IO.Error.mkInvalidArgumentFile : String → UInt32 → String → IO.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 → IO.Error

Equations

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

@[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

Equations

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

@[export lean_mk_io_error_unsupported_operation]

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

Equations

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

@[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

Equations

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

@[export lean_mk_io_error_invalid_argument]

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

Equations

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

@[export lean_mk_io_error_other_error]

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

Equations

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

@[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

Equations

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

@[export lean_mk_io_error_unsatisfied_constraints]

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

Equations

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

@[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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[export lean_io_error_to_string]

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

Equations

• One or more equations did not get rendered due to their size.

instance IO.Error.instToStringError : ToString IO.Error

Equations

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