diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 0cf0ffd6f1..dd468f3e7b 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -133,11 +133,6 @@ constant Handle.read (h : @& Handle) (bytes : USize) : IO ByteArray := arbitrar @[extern "lean_io_prim_handle_write"] constant Handle.write (h : @& Handle) (buffer : @& ByteArray) : IO Unit := arbitrary _ -@[extern "lean_io_prim_handle_read_byte"] -constant Handle.getByte (h : @& Handle) : IO UInt8 := arbitrary _ -@[extern "lean_io_prim_handle_write_byte"] -constant Handle.putByte (h : @& Handle) (c : UInt8) : IO Unit := arbitrary _ - @[extern "lean_io_prim_handle_get_line"] constant Handle.getLine (h : @& Handle) : IO String := arbitrary _ @[extern "lean_io_prim_handle_put_str"] @@ -178,8 +173,6 @@ def Handle.isEof : Handle → m Bool := Prim.liftIO ∘ Prim.Handle.isEof def Handle.flush : Handle → m Unit := Prim.liftIO ∘ Prim.Handle.flush def Handle.read (h : Handle) (bytes : Nat) : m ByteArray := Prim.liftIO (Prim.Handle.read h (USize.ofNat bytes)) def Handle.write (h : Handle) (s : ByteArray) : m Unit := Prim.liftIO (Prim.Handle.write h s) -def Handle.getByte (h : Handle) : m UInt8 := Prim.liftIO (Prim.Handle.getByte h) -def Handle.putByte (h : Handle) (b : UInt8) : m Unit := Prim.liftIO (Prim.Handle.putByte h b) def Handle.getLine : Handle → m String := Prim.liftIO ∘ Prim.Handle.getLine diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index e7f45fc904..d7dfc485e9 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -275,27 +275,6 @@ extern "C" obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /* w */) { } } -/* Handle.readByte : (@& Handle) → IO UInt8 */ -extern "C" obj_res lean_io_prim_handle_read_byte(b_obj_arg h, obj_arg /* w */) { - FILE * fp = io_get_handle(h); - int c = std::fgetc(fp); - if (c != EOF) { - return set_io_result(box(c)); - } else { - return set_io_error(decode_io_error(errno, nullptr)); - } -} - -/* Handle.writeByte : (@& Handle) → UInt8 → IO unit */ -extern "C" obj_res lean_io_prim_handle_write_byte(b_obj_arg h, uint8 c, obj_arg /* w */) { - FILE * fp = io_get_handle(h); - if (std::fputc(c, fp) != EOF) { - return set_io_result(box(0)); - } else { - return set_io_error(decode_io_error(errno, nullptr)); - } -} - static object * g_io_error_eof = nullptr; /* Handle.read : (@& Handle) → USize → IO ByteArray */