chore: move more tests to new frontend

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

tests/lean/run/newfrontend1.lean

@@ -1,6 +1,5 @@
-def x := 1
-
 new_frontend
+def x := 1
 
 #check x
 

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 :=

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 {