Documentation

Init.System.IOError

source
inductive IO.Error:
Type
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