From bebca447735abf00be5831dcd225613b208e0c51 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 18 Nov 2020 17:31:10 -0800
Subject: [PATCH] feat: add `println!` macro for rewriting examples

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

diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 5d66eada39..226eb83227 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -11,6 +11,7 @@ import Init.Data.ByteArray
 import Init.System.IOError
 import Init.System.FilePath
 import Init.System.ST
+import Init.Data.ToString.Macro
 
 /-- Like https://hackage.haskell.org/package/ghc-Prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld.
     Makes sure we never reorder `IO` operations.
@@ -481,3 +482,12 @@ instance {α : Type} [Eval α] : Eval (IO α) :=
   IO.FS.withIsolatedStreams (Eval.eval a false)
 
 end Lean
+
+syntax "println! " (interpolatedStr(term) <|> term) : term
+
+macro_rules
+  | `(println! $msg) =>
+    if msg.getKind == Lean.interpolatedStrKind then
+      `((IO.println (s! $msg) : IO Unit))
+    else
+      `((IO.println $msg : IO Unit))