Module lean_sys::io

IO Helper functions

Functions

lean_decode_io_error^⚠

lean_io_mark_end_initialization^⚠

lean_io_mk_world^⚠

lean_io_result_get_error^⚠

lean_io_result_get_value^⚠

lean_io_result_is_error^⚠

lean_io_result_is_ok^⚠

lean_io_result_mk_error^⚠

lean_io_result_mk_ok^⚠

lean_io_result_show_error^⚠

lean_mk_io_error_already_exists^⚠

lean_mk_io_error_already_exists_file^⚠

lean_mk_io_error_eof^⚠

lean_mk_io_error_hardware_fault^⚠

lean_mk_io_error_illegal_operation^⚠

lean_mk_io_error_inappropriate_type^⚠

lean_mk_io_error_inappropriate_type_file^⚠

lean_mk_io_error_interrupted^⚠

lean_mk_io_error_invalid_argument^⚠

lean_mk_io_error_invalid_argument_file^⚠

lean_mk_io_error_no_file_or_directory^⚠

lean_mk_io_error_no_such_thing^⚠

lean_mk_io_error_no_such_thing_file^⚠

lean_mk_io_error_other_error^⚠

lean_mk_io_error_permission_denied^⚠

lean_mk_io_error_permission_denied_file^⚠

lean_mk_io_error_protocol_error^⚠

lean_mk_io_error_resource_busy^⚠

lean_mk_io_error_resource_exhausted^⚠

lean_mk_io_error_resource_exhausted_file^⚠

lean_mk_io_error_resource_vanished^⚠

lean_mk_io_error_time_expired^⚠

lean_mk_io_error_unsatisfied_constraints^⚠

lean_mk_io_error_unsupported_operation^⚠

lean_mk_io_user_error^⚠