diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 605d892f0d..e51829b1df 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -957,12 +957,14 @@ def Handle.readToEnd (h : Handle) : IO String := do
   | none => throw <| .userError s!"Tried to read from handle containing non UTF-8 data."
 
 /--
-Returns the contents of a UTF-8-encoded text file as an array of lines.
+Reads the entire remaining contents of the file handle as a UTF-8-encoded array of lines.
 
 Newline markers are not included in the lines.
+
+The underlying file is not automatically closed, and subsequent reads from the handle may block
+and/or return data.
 -/
-partial def lines (fname : FilePath) : IO (Array String) := do
-  let h ← Handle.mk fname Mode.read
+partial def Handle.lines (h : Handle) : IO (Array String) := do
   let rec read (lines : Array String) := do
     let line ← h.getLine
     if line.length == 0 then
@@ -975,6 +977,15 @@ partial def lines (fname : FilePath) : IO (Array String) := do
       pure <| lines.push line
   read #[]
 
+/--
+Returns the contents of a UTF-8-encoded text file as an array of lines.
+
+Newline markers are not included in the lines.
+-/
+def lines (fname : FilePath) : IO (Array String) := do
+  let h ← Handle.mk fname Mode.read
+  h.lines
+
 /--
 Write the provided bytes to a binary file at the specified path.
 -/
@@ -1666,6 +1677,27 @@ def ofBuffer (r : Ref Buffer) : Stream where
     { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size }
   isTty   := pure false
 
+/--
+Reads the entire remaining contents of the stream as a UTF-8-encoded array of lines.
+
+Newline markers are not included in the lines.
+
+The underlying stream is not automatically closed, and subsequent reads from the stream may block
+and/or return data.
+-/
+partial def lines (s : Stream) : IO (Array String) := do
+  let rec read (lines : Array String) := do
+    let line ← s.getLine
+    if line.length == 0 then
+      pure lines
+    else if line.back == '\n' then
+      let line := line.dropRight 1
+      let line := if line.back == '\r' then line.dropRight 1 else line
+      read <| lines.push line
+    else
+      pure <| lines.push line
+  read #[]
+
 end Stream
 
 /--