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 (filename : Option String) (osCode : UInt32) (details : String) : IO.Error
• otherError (osCode : UInt32) (details : String) : IO.Error
• resourceBusy (osCode : UInt32) (details : String) : IO.Error
• resourceVanished (osCode : UInt32) (details : String) : IO.Error
• unsupportedOperation (osCode : UInt32) (details : String) : IO.Error
• hardwareFault (osCode : UInt32) (details : String) : IO.Error
• unsatisfiedConstraints (osCode : UInt32) (details : String) : IO.Error
• illegalOperation (osCode : UInt32) (details : String) : IO.Error
• protocolError (osCode : UInt32) (details : String) : IO.Error
• timeExpired (osCode : UInt32) (details : String) : IO.Error
• interrupted (filename : String) (osCode : UInt32) (details : String) : IO.Error
• noFileOrDirectory (filename : String) (osCode : UInt32) (details : String) : IO.Error
• invalidArgument (filename : Option String) (osCode : UInt32) (details : String) : IO.Error
• permissionDenied (filename : Option String) (osCode : UInt32) (details : String) : IO.Error
• resourceExhausted (filename : Option String) (osCode : UInt32) (details : String) : IO.Error
• inappropriateType (filename : Option String) (osCode : UInt32) (details : String) : IO.Error
• noSuchThing (filename : Option String) (osCode : UInt32) (details : String) : IO.Error
• unexpectedEof : IO.Error
• userError (msg : 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

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

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

Equations

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