From 4b37c5ad04b78e2a396d13ef424e06bdf8d58142 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Jan 2020 21:02:25 -0800
Subject: [PATCH] test: add `new_frontend` command test

---
 tests/lean/run/newfrontend1.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 tests/lean/run/newfrontend1.lean

diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
new file mode 100644
index 0000000000..2ec5d919b6
--- /dev/null
+++ b/tests/lean/run/newfrontend1.lean
@@ -0,0 +1,17 @@
+def x := 1
+
+new_frontend
+
+#check x
+
+variables {α : Type}
+
+def f (a : α) : α :=
+a
+
+def tst (xs : List Nat) : Nat :=
+xs.foldl (init := 10) (· + ·)
+
+#check tst [1, 2, 3]
+
+#check tst