From 50ce4e8ae928075d73106b14841fa7c21d35943a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 5 Jun 2018 16:29:12 -0700
Subject: [PATCH] chore(library/init/meta/interactive_base): remove Lean3
 format macros

---
 library/init/meta/interactive_base.lean | 38 -------------------------
 1 file changed, 38 deletions(-)

diff --git a/library/init/meta/interactive_base.lean b/library/init/meta/interactive_base.lean
index 48aa8c07ca..0f5aa3da4b 100644
--- a/library/init/meta/interactive_base.lean
+++ b/library/init/meta/interactive_base.lean
@@ -200,41 +200,3 @@ meta structure inductive_decl :=
 meta constant inductive_decl.parse : decl_meta_info → parser inductive_decl
 
 end interactive
-
-section macros
-open interaction_monad
-open interactive
-
-private meta def parse_format : string → list char → parser pexpr
-| acc []            := pure ``(to_fmt %%(reflect acc))
-| acc ('\n'::s)     :=
-do f ← parse_format "" s,
-   pure ``(to_fmt %%(reflect acc) ++ format.line ++ %%f)
-| acc ('{'::'{'::s) := parse_format (acc ++ "{") s
-| acc ('{'::s) :=
-do (e, s) ← with_input (lean3.parser.pexpr 0) s.as_string,
-   '}'::s ← return s.to_list | fail "'}' expected",
-   f ← parse_format "" s,
-   pure ``(to_fmt %%(reflect acc) ++ to_fmt %%e ++ %%f)
-| acc (c::s) := parse_format (acc.str c) s
-
-reserve prefix `format! `:100
-@[user_notation]
-meta def format_macro (_ : parse $ tk "format!") (s : string) : parser pexpr :=
-parse_format "" s.to_list
-
-private meta def parse_sformat : string → list char → parser pexpr
-| acc []            := pure $ pexpr.of_expr (reflect acc)
-| acc ('{'::'{'::s) := parse_sformat (acc ++ "{") s
-| acc ('{'::s) :=
-do (e, s) ← with_input (lean3.parser.pexpr 0) s.as_string,
-   '}'::s ← return s.to_list | fail "'}' expected",
-   f ← parse_sformat "" s,
-   pure ``(%%(reflect acc) ++ to_string %%e ++ %%f)
-| acc (c::s) := parse_sformat (acc.str c) s
-
-reserve prefix `sformat! `:100
-@[user_notation]
-meta def sformat_macro (_ : parse $ tk "sformat!") (s : string) : parser pexpr :=
-parse_sformat "" s.to_list
-end macros