diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 4a3d0c5bce8b..3353e9f8683b 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -311,6 +311,8 @@ Note that EOF does not actually close a stream, so further reads may block and r
   -/
   getLine : IO String
   putStr  : String → IO Unit
+  /-- Returns true if a stream refers to a Windows console or Unix terminal. -/
+  isTty   : BaseIO Bool
   deriving Inhabited
 
 open FS
@@ -360,6 +362,9 @@ Will succeed even if no lock has been acquired.
 -/
 @[extern "lean_io_prim_handle_unlock"] opaque unlock (h : @& Handle) : IO Unit
 
+/-- Returns true if a handle refers to a Windows console or Unix terminal. -/
+@[extern "lean_io_prim_handle_is_tty"] opaque isTty (h : @& Handle) : BaseIO Bool
+
 @[extern "lean_io_prim_handle_flush"] opaque flush (h : @& Handle) : IO Unit
 /-- Rewinds the read/write cursor to the beginning of the handle. -/
 @[extern "lean_io_prim_handle_rewind"] opaque rewind (h : @& Handle) : IO Unit
@@ -743,36 +748,37 @@ namespace FS
 namespace Stream
 
 @[export lean_stream_of_handle]
-def ofHandle (h : Handle) : Stream := {
-  flush   := Handle.flush h,
-  read    := Handle.read h,
-  write   := Handle.write h,
-  getLine := Handle.getLine h,
-  putStr  := Handle.putStr h,
-}
+def ofHandle (h : Handle) : Stream where
+  flush   := Handle.flush h
+  read    := Handle.read h
+  write   := Handle.write h
+  getLine := Handle.getLine h
+  putStr  := Handle.putStr h
+  isTty   := Handle.isTty h
 
 structure Buffer where
   data : ByteArray := ByteArray.empty
   pos  : Nat := 0
 
-def ofBuffer (r : Ref Buffer) : Stream := {
-  flush   := pure (),
+def ofBuffer (r : Ref Buffer) : Stream where
+  flush   := pure ()
   read    := fun n => r.modifyGet fun b =>
     let data := b.data.extract b.pos (b.pos + n.toNat)
-    (data, { b with pos := b.pos + data.size }),
+    (data, { b with pos := b.pos + data.size })
   write   := fun data => r.modify fun b =>
     -- set `exact` to `false` so that repeatedly writing to the stream does not impose quadratic run time
-    { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size },
+    { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size }
   getLine := r.modifyGet fun b =>
     let pos := match b.data.findIdx? (start := b.pos) fun u => u == 0 || u = '\n'.toNat.toUInt8 with
       -- include '\n', but not '\0'
       | some pos => if b.data.get! pos == 0 then pos else pos + 1
       | none     => b.data.size
-    (String.fromUTF8Unchecked <| b.data.extract b.pos pos, { b with pos := pos }),
+    (String.fromUTF8Unchecked <| b.data.extract b.pos pos, { b with pos := pos })
   putStr  := fun s => r.modify fun b =>
     let data := s.toUTF8
-    { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size },
-}
+    { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size }
+  isTty   := pure false
+
 end Stream
 
 /-- Run action with `stdin` emptied and `stdout+stderr` captured into a `String`. -/
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 2b3fb8e7cfe3..4dddd7afc0b5 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -302,11 +302,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_mk(b_obj_arg filename, uint8
 #ifdef LEAN_WINDOWS
 
 static inline HANDLE win_handle(FILE * fp) {
-#ifdef q4_WCE
-    return (HANDLE)_fileno(fp);
-#else
     return (HANDLE)_get_osfhandle(_fileno(fp));
-#endif
 }
 
 /* Handle.lock : (@& Handle) → (exclusive : Bool) → IO Unit */
@@ -391,13 +387,41 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h, obj_arg /
 
 #endif
 
+/* Handle.isTty : (@& Handle) → BaseIO Bool */
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_is_tty(b_obj_arg h, obj_arg /* w */) {
+    FILE * fp = io_get_handle(h);
+#ifdef LEAN_WINDOWS
+    /*
+    On Windows, there are two approaches for detecting a console.
+    1)  _isatty(_fileno(fp)) != 0
+        This checks whether the file descriptor is a *character device*,
+        not just a terminal (unlike Unix's isatty). Thus, it produces a false
+        positive in some edge cases (such as NUL).
+        https://stackoverflow.com/q/3648711
+    2)  GetConsoleMode(win_handle(fp), &mode) != 0
+        Errors if the handle is not a console. Unfortunately, this produces
+        a false negative for a terminal emulator like MSYS/Cygwin's Mintty,
+        which is not implemented as a Windows-recognized console on
+        old Windows versions (e.g., pre-Windows 10, pre-ConPTY).
+        https://github.com/msys2/MINGW-packages/issues/14087
+    We choose to use GetConsoleMode as that seems like the more modern approach,
+    and Lean does not support pre-Windows 10.
+    */
+    DWORD mode;
+    return io_result_mk_ok(box(GetConsoleMode(win_handle(fp), &mode) != 0));
+#else
+    // We ignore errors for consistency with Windows.
+    return io_result_mk_ok(box(isatty(fileno(fp))));
+#endif
+}
+
 /* Handle.isEof : (@& Handle) → BaseIO Bool */
 extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_is_eof(b_obj_arg h, obj_arg /* w */) {
     FILE * fp = io_get_handle(h);
     return io_result_mk_ok(box(std::feof(fp) != 0));
 }
 
-/* Handle.flush : (@& Handle) → IO Bool */
+/* Handle.flush : (@& Handle) → IO Unit */
 extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /* w */) {
     FILE * fp = io_get_handle(h);
     if (!std::fflush(fp)) {