Documentation

Init.System.IOError

source
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

Instances For
    source
    instance IO.instInhabitedError :
    Inhabited IO.Error
    Equations
    source
    @[export lean_mk_io_user_error]
    def IO.userError (s : String) :
    IO.Error
    Equations
    source
    instance instCoeStringError :
    Coe String IO.Error
    Equations
    source
    @[export lean_mk_io_error_already_exists_file]
    def IO.Error.mkAlreadyExistsFile :
    String → UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_eof]
    def IO.Error.mkEofError :
    Unit → IO.Error
    Equations
    source
    @[export lean_mk_io_error_inappropriate_type_file]
    def IO.Error.mkInappropriateTypeFile :
    String → UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_interrupted]
    def IO.Error.mkInterrupted :
    String → UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_invalid_argument_file]
    def IO.Error.mkInvalidArgumentFile :
    String → UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_no_file_or_directory]
    def IO.Error.mkNoFileOrDirectory :
    String → UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_no_such_thing_file]
    def IO.Error.mkNoSuchThingFile :
    String → UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_permission_denied_file]
    def IO.Error.mkPermissionDeniedFile :
    String → UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_resource_exhausted_file]
    def IO.Error.mkResourceExhaustedFile :
    String → UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_unsupported_operation]
    def IO.Error.mkUnsupportedOperation :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_resource_exhausted]
    def IO.Error.mkResourceExhausted :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_already_exists]
    def IO.Error.mkAlreadyExists :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_inappropriate_type]
    def IO.Error.mkInappropriateType :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_no_such_thing]
    def IO.Error.mkNoSuchThing :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_resource_vanished]
    def IO.Error.mkResourceVanished :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_resource_busy]
    def IO.Error.mkResourceBusy :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_invalid_argument]
    def IO.Error.mkInvalidArgument :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_other_error]
    def IO.Error.mkOtherError :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_permission_denied]
    def IO.Error.mkPermissionDenied :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_hardware_fault]
    def IO.Error.mkHardwareFault :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_unsatisfied_constraints]
    def IO.Error.mkUnsatisfiedConstraints :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_illegal_operation]
    def IO.Error.mkIllegalOperation :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_protocol_error]
    def IO.Error.mkProtocolError :
    UInt32 → String → IO.Error
    Equations
    source
    @[export lean_mk_io_error_time_expired]
    def IO.Error.mkTimeExpired :
    UInt32 → String → IO.Error
    Equations
    source
    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.
    source
    def IO.Error.otherErrorToString (gist : String) (code : UInt32) :
    Option String → String
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[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.
    source
    instance IO.Error.instToStringError :
    ToString IO.Error
    Equations