From 5e0121c8dc14d0db28cc337aa6bb4eabcbb31005 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Oct 2020 15:29:15 -0700
Subject: [PATCH] feat: add `f!<interpolated string>` macro for `Format`

---
 src/Lean/Data/FormatMacro.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 src/Lean/Data/FormatMacro.lean

diff --git a/src/Lean/Data/FormatMacro.lean b/src/Lean/Data/FormatMacro.lean
new file mode 100644
index 0000000000..2ef4eb05ef
--- /dev/null
+++ b/src/Lean/Data/FormatMacro.lean
@@ -0,0 +1,18 @@
+#lang lean4
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Data.Format
+namespace Lean
+
+syntax:max "f!" (interpolatedStr term) : term
+
+macro_rules
+| `(f! $interpStr) => do
+  let chunks := interpStr.getArgs
+  let r ← Lean.Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(fmt $a))
+  `(($r : Format))
+
+end Lean