From a3f5aca22f05f2e1a19e2608812ed965c38981a2 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Thu, 21 Jan 2021 14:54:14 -0500
Subject: [PATCH] fix: tail-recursive readBinToEnd

---
 src/Init/System/IO.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 9810901730..abe78b951a 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -214,13 +214,13 @@ def Handle.putStrLn (h : Handle) (s : String) : m Unit :=
   h.putStr (s.push '\n')
 
 partial def Handle.readBinToEnd (h : Handle) : m ByteArray := do
-  let rec loop : m ByteArray := do
+  let rec loop (acc : ByteArray) : m ByteArray := do
     if ← h.isEof then
-      return ByteArray.empty
+      return acc
     else
       let buf ← h.read 1024
-      return buf ++ (←loop)
-  loop
+      loop (acc ++ buf)
+  loop ByteArray.empty
 
 partial def Handle.readToEnd (h : Handle) : m String := do
   let rec read (s : String) := do