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

tests/lean/run/cases_tac1.lean

@@ -1,3 +1,5 @@
+set_option new_elaborator true
+
 inductive vec (A : Type*) : nat → Type*
 | nil  : vec 0
 | cons : ∀ {n}, A → vec n → vec (n+1)

tests/lean/run/class1.lean

@@ -1,5 +1,7 @@
+set_option new_elaborator true
 open prod inhabited
 
-definition H : inhabited (Prop × num × (num → num)) := _
+definition H : inhabited (Prop × num × (num → num)) :=
+by tactic.apply_instance
 
 print H

tests/lean/run/class2.lean

@@ -1,6 +1,7 @@
-open prod nonempty inhabited
-
+set_option new_elaborator true
+open tactic
 theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
-:= _
+:= by apply_instance
+
 reveal H
 print H

tests/lean/run/class3.lean

@@ -1,4 +1,5 @@
-open prod inhabited
+set_option new_elaborator true
+open tactic
 
 section
   variable {A : Type}
@@ -6,7 +7,7 @@ section
   variable Ha : inhabited A
   variable Hb : inhabited B
   include Ha Hb
-  theorem tst : inhabited (Prop × A × B)
+  theorem tst : inhabited (Prop × A × B) := by apply_instance
 
 end
 

tests/lean/run/class6.lean

@@ -1,4 +1,5 @@
-open prod
+set_option new_elaborator true
+open tactic
 
 inductive t1 : Type
 | mk1 : t1
@@ -12,8 +13,8 @@ theorem inhabited_t1 : inhabited t1
 theorem inhabited_t2 : inhabited t2
 := inhabited.mk t2.mk2
 
-attribute inhabited_t1 [instance]
-attribute inhabited_t2 [instance]
+attribute [instance] inhabited_t1
+attribute [instance] inhabited_t2
 
 theorem T : inhabited (t1 × t2)
-:= _
+:= by apply_instance

tests/lean/run/contra3.lean

@@ -1,3 +1,4 @@
+set_option new_elaborator true
 open tactic nat
 
 example (a b c : Prop) : a → b → ¬ a → c :=
@@ -6,8 +7,8 @@ by do intros, contradiction
 example (a b c : Prop) : a → false → b → c :=
 by do intros, contradiction
 
-example (a b : nat) : succ a = zero → b = 0 :=
+example (a b : nat) : succ a = 0 → b = 0 :=
 by do intro `H, contradiction
 
-example (a b : nat) : succ a = succ b → succ a = zero → b = 0 :=
+example (a b : nat) : succ a = succ b → succ a = 0 → b = 0 :=
 by do intros, contradiction

tests/lean/run/empty_eq.lean

@@ -1,3 +1,4 @@
+set_option new_elaborator true
 open nat
 
 inductive Fin : nat → Type
@@ -6,8 +7,8 @@ inductive Fin : nat → Type
 
 open Fin
 
-definition case0 {C : Fin zero → Type} : Π (f : Fin zero), C f
-| [none]
+definition case0 {C : Fin 0 → Type} : Π (f : Fin 0), C f
+.
 
 
 print definition case0

tests/lean/run/match_fun.lean

@@ -1,20 +1,20 @@
+set_option new_elaborator true
 open bool nat
 
 definition foo (b : bool) : nat → nat :=
 match b with
-| tt := λ x : nat, zero
-| ff := λ y : nat, (succ zero)
+| tt := λ x : nat, 0
+| ff := λ y : nat, (succ 0)
 end
 
-example : foo tt 1 = zero := rfl
+example : foo tt 1 = 0 := rfl
 example : foo ff 1 = 1 := rfl
 
-
-definition zero_fn := λ x : nat, zero
+definition zero_fn := λ x : nat, 0
 
 definition foo2 : bool → nat → nat
-| foo2 tt := succ
-| foo2 ff := zero_fn
+| tt := succ
+| ff := zero_fn
 
 example : foo2 tt 1 = 2 := rfl
 example : foo2 tt 2 = 3 := rfl

tests/lean/run/nat_bug.lean

@@ -1,5 +1,5 @@
-open decidable
-open eq
+set_option new_elaborator true
+open decidable open eq
 namespace experiment
 inductive nat : Type
 | zero : nat
@@ -7,7 +7,7 @@ inductive nat : Type
 definition refl := @eq.refl
 namespace nat
 
-definition pred (n : nat) := nat.rec zero (fun m x, m) n
+definition pred (n : nat) : nat := nat.rec zero (fun m x, m) n
 theorem pred_zero : pred zero = zero := refl _
 theorem pred_succ (n : nat) : pred (succ n) = n := refl _
 
@@ -18,7 +18,7 @@ theorem zero_or_succ (n : nat) : n = zero ∨ n = succ (pred n)
       (show succ m = succ (pred (succ m)), from congr_arg succ (symm (pred_succ m))))
 
 theorem zero_or_succ2 (n : nat) : n = zero ∨ n = succ (pred n)
-:= @nat.induction_on _ n
+:= nat.induction_on n
     (or.intro_left _ (refl zero))
     (take m IH, or.intro_right _
       (show succ m = succ (pred (succ m)), from congr_arg succ (symm (pred_succ m))))