chore(tests/lean/run): move tests to new elaborator

tests/lean/run/e4.lean

@@ -1,4 +1,5 @@
 prelude
+set_option new_elaborator true
 definition Prop := Type.{0}
 
 definition false : Prop := ∀x : Prop, x
@@ -23,6 +24,7 @@ definition true : Prop
 theorem trivial : true
 := refl false
 
+attribute [elab_as_eliminator]
 theorem subst {A : Type} {P : A -> Prop} {a b : A} (H1 : a = b) (H2 : P a) : P b
 := H1 _ H2
 

tests/lean/run/empty_match.lean

@@ -1,7 +1,8 @@
+set_option new_elaborator true
 open nat
 
-definition not_lt_zero (a : nat) : ¬ a < zero :=
-assume H : a < zero,
+definition not_lt_zero (a : nat) : ¬ a < 0 :=
+assume H : a < 0,
 match H with
 end
 

tests/lean/run/meta2.lean

@@ -1,9 +1,10 @@
 import system.IO
+set_option new_elaborator true
 
-meta_definition foo (a : nat) : nat :=
-nat.cases_on a 1 (λ n, foo n + 2)
+meta_definition foo : nat → nat
+| a := nat.cases_on a 1 (λ n, foo n + 2)
 
 vm_eval (foo 10)
 
-meta_definition loop (a : nat) : IO unit :=
-do put_str ">> ", put_nat a, put_str "\n", loop (a+1)
+meta_definition loop : nat → IO unit
+| a := do put_str ">> ", put_nat a, put_str "\n", loop (a+1)

tests/lean/run/meta_tac1.lean

@@ -1,3 +1,4 @@
+set_option new_elaborator true
 set_option pp.all true
 
 open tactic list

tests/lean/run/occurs_check_bug1.lean

@@ -1,3 +1,4 @@
+set_option new_elaborator true
 open nat prod
 open decidable
 
@@ -14,4 +15,4 @@ sorry
 constant succ_ne_zero (a : nat) : succ a ≠ 0
 
 theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) :=
-eq.trans (gcd_def _ _) (if_neg (succ_ne_zero _))
+eq.trans (gcd_def _ _) (if_neg (nat.succ_ne_zero _))