From b40ef65b39842c9ea4600e13ec47116d7c497569 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 4 Jul 2020 19:15:26 +0200
Subject: [PATCH] feat: add IO.eprint(ln) for printing to stderr

Most useful when stdout is being consumed by another program
---
 src/Init/System/IO.lean | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index bfae9e2a10..51507953fa 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -232,12 +232,18 @@ Prim.liftIO Prim.stdout
 def stderr : m FS.Handle :=
 Prim.liftIO Prim.stderr
 
-private def putStr (s : String) : m Unit := do
+def print {α} [HasToString α] (s : α) : m Unit := do
 out ← stdout;
-out.putStr s
+out.putStr $ toString s
+
+def println {α} [HasToString α] (s : α) : m Unit := print s *> print "\n"
+
+def eprint {α} [HasToString α] (s : α) : m Unit := do
+out ← stderr;
+out.putStr $ toString s
+
+def eprintln {α} [HasToString α] (s : α) : m Unit := eprint s *> eprint "\n"
 
-def print {α} [HasToString α] (s : α) : m Unit := putStr ∘ toString $ s
-def println {α} [HasToString α] (s : α) : m Unit := print s *> putStr "\n"
 def getEnv : String → m (Option String) := Prim.liftIO ∘ Prim.getEnv
 def realPath : String → m String := Prim.liftIO ∘ Prim.realPath
 def isDir : String → m Bool := Prim.liftIO ∘ Prim.isDir