From 6bfecdf00cdda479799ce4da9f0ab07141e411a5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 18 Sep 2016 19:10:48 -0700
Subject: [PATCH] chore(tests/lean/run): move tests to new elaborator

---
 tests/lean/run/e4.lean                | 2 ++
 tests/lean/run/empty_match.lean       | 5 +++--
 tests/lean/run/meta2.lean             | 9 +++++----
 tests/lean/run/meta_tac1.lean         | 1 +
 tests/lean/run/occurs_check_bug1.lean | 3 ++-
 5 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/tests/lean/run/e4.lean b/tests/lean/run/e4.lean
index 077d1b699f..255c8d4af1 100644
--- a/tests/lean/run/e4.lean
+++ b/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
 
diff --git a/tests/lean/run/empty_match.lean b/tests/lean/run/empty_match.lean
index 8af215a264..5d9a344270 100644
--- a/tests/lean/run/empty_match.lean
+++ b/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
 
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 797e7bb62a..4adb0e6463 100644
--- a/tests/lean/run/meta2.lean
+++ b/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)
diff --git a/tests/lean/run/meta_tac1.lean b/tests/lean/run/meta_tac1.lean
index 2207e8f60f..d62cfcee5b 100644
--- a/tests/lean/run/meta_tac1.lean
+++ b/tests/lean/run/meta_tac1.lean
@@ -1,3 +1,4 @@
+set_option new_elaborator true
 set_option pp.all true
 
 open tactic list
diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean
index 1dfb4040d3..398eaff4c3 100644
--- a/tests/lean/run/occurs_check_bug1.lean
+++ b/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 _))