From 233a787e651aefac83c602f167dd10bc5701ff03 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 23 Jun 2022 21:50:18 +0200
Subject: [PATCH] chore: add test for sepByIndent.formatter

---
 tests/lean/sepByIndentQuot.lean              | 16 ++++++++++++++++
 tests/lean/sepByIndentQuot.lean.expected.out |  6 ++++++
 2 files changed, 22 insertions(+)
 create mode 100644 tests/lean/sepByIndentQuot.lean
 create mode 100644 tests/lean/sepByIndentQuot.lean.expected.out

diff --git a/tests/lean/sepByIndentQuot.lean b/tests/lean/sepByIndentQuot.lean
new file mode 100644
index 0000000000..f85458a319
--- /dev/null
+++ b/tests/lean/sepByIndentQuot.lean
@@ -0,0 +1,16 @@
+import Lean
+open Lean Elab
+
+#eval show TermElabM _ from do
+  let x ← `(x)
+  let xs := #[x,x,x,x]
+  let ys := xs
+  PrettyPrinter.ppTerm <|<-
+    `(frobnicate { $[$xs:ident := $ys:term],* })
+
+#eval show TermElabM _ from do
+  let x ← `(x)
+  let xs := #[x,x,x,x]
+  let ys := xs
+  PrettyPrinter.ppTerm <|<-
+    `(frobnicate { $[$xs:ident := $ys:term]* })
diff --git a/tests/lean/sepByIndentQuot.lean.expected.out b/tests/lean/sepByIndentQuot.lean.expected.out
new file mode 100644
index 0000000000..51b92c6a06
--- /dev/null
+++ b/tests/lean/sepByIndentQuot.lean.expected.out
@@ -0,0 +1,6 @@
+frobnicate✝ { x✝ := x✝, x✝ := x✝, x✝ := x✝, x✝ := x✝ }
+frobnicate✝ { 
+  x✝ := x✝
+  x✝ := x✝
+  x✝ := x✝
+  x✝ := x✝ }