diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index a1143f2a97..c923a12a38 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -660,7 +660,15 @@ extern "C" LEAN_EXPORT obj_res lean_io_remove_dir(b_obj_arg p, obj_arg) {
 }
 
 extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean_object * /* w */) {
-    if (std::rename(string_cstr(from), string_cstr(to)) == 0) {
+#ifdef LEAN_WINDOWS
+    // Note: On windows, std::rename gives an error if the `to` file already exists,
+    // so we have to call the underlying windows API directly to get behavior consistent
+    // with the unix-like OSs
+    bool ok = MoveFileEx(string_cstr(from), string_cstr(to), MOVEFILE_REPLACE_EXISTING) != 0;
+#else
+    bool ok = std::rename(string_cstr(from), string_cstr(to)) == 0;
+#endif
+    if (ok) {
         return io_result_mk_ok(box(0));
     } else {
         std::ostringstream s;
diff --git a/tests/lean/run/IO_test.lean b/tests/lean/run/IO_test.lean
index 28271470e5..949fa38a19 100644
--- a/tests/lean/run/IO_test.lean
+++ b/tests/lean/run/IO_test.lean
@@ -35,6 +35,7 @@ pure ()
 #eval test
 
 def test2 : IO Unit := do
+let fn1 := "bar2.txt";
 let fn2 := "foo2.txt";
 let xs₀ : String := "⟨[₂,α]⟩";
 let xs₁ := "⟨[6,8,@]⟩";
@@ -43,14 +44,15 @@ let xs₂ := "/* Handle.getLine : Handle → IO Unit                     */" ++
            "/*   is truncated at the first \'\\0\' character and the    */" ++
            "/*   rest of the line is discarded.                      */";
     -- multi-buffer line
-withFile fn2 Mode.write $ fun h => pure ();
+withFile fn1 Mode.write $ fun _h => pure ();
 
-withFile fn2 Mode.write $ fun h => do
-{ h.putStr xs₀;
-  h.putStrLn xs₀;
-  h.putStrLn xs₂;
-  h.putStrLn xs₁;
-  pure () };
+withFile fn1 Mode.write $ fun h => do
+  h.putStr xs₀
+  h.putStrLn xs₀
+  h.putStrLn xs₂
+  h.putStrLn xs₁
+withFile fn2 Mode.write $ fun h => h.putStr "overwritten"
+rename fn1 fn2
 let ys ← withFile fn2 Mode.read $ fun h => h.getLine;
 IO.println ys;
 check_eq "1" (xs₀ ++ xs₀ ++ "\n") ys;
@@ -80,7 +82,7 @@ let xs₀ := "abc"
 let xs₁ := ""
 let xs₂ := "hello"
 let xs₃ := "world"
-withFile fn3 Mode.write $ fun h => do {
+withFile fn3 Mode.write $ fun _h => do {
   pure ()
 }
 let ys ← lines fn3
@@ -100,7 +102,7 @@ pure ()
 
 def test4 : IO Unit := do
 let fn4 := "foo4.txt"
-withFile fn4 Mode.write fun h => do pure ();
+withFile fn4 Mode.write fun _h => do pure ();
 let ys ← withFile fn4 Mode.read $ fun h => h.read 1;
 check_eq "1" [] ys.toList
 let ys ← withFile fn4 Mode.read $ fun h => h.read 1;