From bbc3bec53b98ec72b4d412dac9f7c12d6ee4b731 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 11 Sep 2020 16:28:57 -0700
Subject: [PATCH] chore: move more tests to new frontend

---
 tests/lean/run/new_inductive2.lean | 14 ++++++++++----
 tests/lean/run/newfrontend1.lean   |  3 +--
 tests/lean/run/newfrontend2.lean   |  4 ++--
 tests/lean/run/newfrontend3.lean   |  8 ++++----
 4 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/tests/lean/run/new_inductive2.lean b/tests/lean/run/new_inductive2.lean
index 71ff78d214..e08dec06cb 100644
--- a/tests/lean/run/new_inductive2.lean
+++ b/tests/lean/run/new_inductive2.lean
@@ -1,7 +1,9 @@
+new_frontend
+
 universes u v
 
 inductive arrow (α : Type u) (β : Type v)
-| mk : (α → β) → arrow
+| mk : (α → β) → arrow α β
 
 inductive foo
 | mk : arrow Nat foo → foo
@@ -11,10 +13,14 @@ inductive foo
 set_option pp.all true
 #print foo.below
 
-mutual inductive foo2, arrow2
-with foo2 : Type
+mutual
+
+inductive foo2 : Type
 | mk : arrow2 → foo2
-with arrow2 : Type
+
+inductive arrow2 : Type
 | mk : (Nat → foo2) → arrow2
 
+end
+
 #print foo2.brecOn
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index cc3660d434..60a4d6ee41 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -1,6 +1,5 @@
-def x := 1
-
 new_frontend
+def x := 1
 
 #check x
 
diff --git a/tests/lean/run/newfrontend2.lean b/tests/lean/run/newfrontend2.lean
index 4a5d3c70f8..8ded42cfd4 100644
--- a/tests/lean/run/newfrontend2.lean
+++ b/tests/lean/run/newfrontend2.lean
@@ -1,3 +1,5 @@
+new_frontend
+
 def foo {α} (a : Option α) (b : α) : α  :=
 match a with
 | some a => a
@@ -6,8 +8,6 @@ match a with
 structure S :=
 (x : Nat)
 
-new_frontend
-
 #check if 0 == 1 then true else false
 
 def f (x : Nat) : Nat :=
diff --git a/tests/lean/run/newfrontend3.lean b/tests/lean/run/newfrontend3.lean
index 11a86ff3bd..a37b013e91 100644
--- a/tests/lean/run/newfrontend3.lean
+++ b/tests/lean/run/newfrontend3.lean
@@ -1,13 +1,13 @@
+new_frontend
+
 structure S  :=
 (g {α} : α → α)
 
-def f (h : Nat → (forall {α : Type}, α → α) × Bool) : Nat :=
+def f (h : Nat → ({α : Type} → α → α) × Bool) : Nat :=
 (h 0).1 1
 
-new_frontend
-
 def tst : Nat :=
-f (fun n => (fun x => x, true))
+f fun n => (fun x => x, true)
 
 theorem ex : id (Nat → Nat) :=
 by {