From 308bc8de4abdea4c0e9542773d0d30ea29270e05 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Nov 2017 16:59:09 -0800
Subject: [PATCH] chore(tests/lean): fix test suite

---
 tests/lean/inaccessible2.lean                | 2 +-
 tests/lean/inaccessible2.lean.expected.out   | 4 ++--
 tests/lean/notation2.lean.expected.out       | 1 +
 tests/lean/run/bug6.lean                     | 1 -
 tests/lean/run/choice_ctx.lean               | 7 ++++---
 tests/lean/run/cody2.lean                    | 3 +--
 tests/lean/run/eq2.lean                      | 2 ++
 tests/lean/run/imp3.lean                     | 2 ++
 tests/lean/run/inst_bug.lean                 | 2 ++
 tests/lean/run/nat_bug.lean                  | 2 +-
 tests/lean/run/pred_using_structure_cmd.lean | 3 ++-
 tests/lean/run/simp_univ_poly.lean           | 4 +++-
 12 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/tests/lean/inaccessible2.lean b/tests/lean/inaccessible2.lean
index 6cf946e1f1..1dcb8c4dec 100644
--- a/tests/lean/inaccessible2.lean
+++ b/tests/lean/inaccessible2.lean
@@ -10,7 +10,7 @@ definition inv_2 {A B : Sort*} (f : A → B) : ∀ (b : B), imf f b → A
 definition inv_3 {A B : Sort*} (f : A → B) : ∀ (b : B), imf f b → A
 | .(f a) ((λ (x : imf f b), x) (imf.mk .(f) a)) := a  -- Error invalid occurrence of 'lambda' expression
 
-definition symm {A : Sort*} : ∀ a b : A, a = b → b = a
+definition sym {A : Sort*} : ∀ a b : A, a = b → b = a
 | .(a) .(a) (eq.refl a) := rfl -- Error `a` in eq.refl must be marked as inaccessible since it is an inductive datatype parameter
 
 definition symm2 {A : Sort*} : ∀ a b : A, a = b → b = a
diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out
index a1e0214203..df28170bdb 100644
--- a/tests/lean/inaccessible2.lean.expected.out
+++ b/tests/lean/inaccessible2.lean.expected.out
@@ -10,9 +10,9 @@ inaccessible2.lean:11:46: error: command expected
 inaccessible2.lean:14:21: error: don't know how to synthesize placeholder
 context:
 A : Sort ?,
-symm : ∀ (a b : A), a = b → b = a
+sym : ∀ (a b : A), a = b → b = a
 ⊢ A
-inaccessible2.lean:13:11: error: equation compiler failed to create auxiliary declaration 'symm._main'
+inaccessible2.lean:13:11: error: equation compiler failed to create auxiliary declaration 'sym._main'
 nested exception message:
 type mismatch at application
   eq.rec (λ (a_1 : a = a) (H_2 : a_1 == eq.refl a), id_rhs (⁇ = ⁇) rfl)
diff --git a/tests/lean/notation2.lean.expected.out b/tests/lean/notation2.lean.expected.out
index 998e288fee..d4ee854923 100644
--- a/tests/lean/notation2.lean.expected.out
+++ b/tests/lean/notation2.lean.expected.out
@@ -3,3 +3,4 @@
 `[`:1024 (foldr 0 `,`) `]`:0 := #0
 `-[1+`:1024 _:1 `]`:0 := int.neg_succ_of_nat #0
 _ `^[`:1 _:1 `]`:0 := nat.iterate #1 #0
+_ `≈[`:50 _:1 `]`:0 _:50 := @strict_weak_order.equiv _ #1 _ #2 #0
diff --git a/tests/lean/run/bug6.lean b/tests/lean/run/bug6.lean
index 6e58b339d1..479b942bd3 100644
--- a/tests/lean/run/bug6.lean
+++ b/tests/lean/run/bug6.lean
@@ -1,4 +1,3 @@
-open eq
 section
   variable {A : Type}
   theorem T {a b : A} (H : a = b) : b = a
diff --git a/tests/lean/run/choice_ctx.lean b/tests/lean/run/choice_ctx.lean
index 1b19094ae5..8d76f2bc4e 100644
--- a/tests/lean/run/choice_ctx.lean
+++ b/tests/lean/run/choice_ctx.lean
@@ -1,17 +1,18 @@
+namespace test
 open nat
-open eq
 set_option pp.coercions true
 namespace foo
 theorem trans {a b c : nat} (H1 : a = b) (H2 : b = c) : a = c :=
-trans H1 H2
+eq.trans H1 H2
 end foo
 
 open foo
 
 theorem tst (a b : nat) (H0 : b = a) (H : b = 0) : a = 0
-:= have H1 : a = b, from symm H0,
+:= have H1 : a = b, from eq.symm H0,
    foo.trans H1 H
 
 definition f (a b : nat) :=
 let x := 3 in
 a + x
+end test
diff --git a/tests/lean/run/cody2.lean b/tests/lean/run/cody2.lean
index ff2e456e21..c4a984daf5 100644
--- a/tests/lean/run/cody2.lean
+++ b/tests/lean/run/cody2.lean
@@ -1,4 +1,3 @@
-open eq
 definition subsets (P : Type) := P → Prop.
 
 section
@@ -17,7 +16,7 @@ local notation `δ` := delta.
 
 theorem delta_aux : ¬ (δ (i delta))
          := assume H : δ (i delta),
-            H (subst (symm (@retract delta (i delta))) H)
+            H (eq.subst (symm (@retract delta (i delta))) H)
 
 #check delta_aux.
 
diff --git a/tests/lean/run/eq2.lean b/tests/lean/run/eq2.lean
index e56c577337..63b0dbf689 100644
--- a/tests/lean/run/eq2.lean
+++ b/tests/lean/run/eq2.lean
@@ -1,5 +1,7 @@
+namespace test
 definition symm {A : Type} : Π {a b : A}, a = b → b = a
 | a .(a) rfl := rfl
 
 definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c
 | a .(a) .(a) rfl rfl := rfl
+end test
diff --git a/tests/lean/run/imp3.lean b/tests/lean/run/imp3.lean
index c413200b8d..228573394b 100644
--- a/tests/lean/run/imp3.lean
+++ b/tests/lean/run/imp3.lean
@@ -1,3 +1,4 @@
+namespace old
 class is_equiv {A B : Type} (f : A → B) :=
   (inv : B → A)
 
@@ -10,3 +11,4 @@ section
    #check inv f
 end
 end is_equiv
+end old
diff --git a/tests/lean/run/inst_bug.lean b/tests/lean/run/inst_bug.lean
index 2041c270d4..2d07f7b96d 100644
--- a/tests/lean/run/inst_bug.lean
+++ b/tests/lean/run/inst_bug.lean
@@ -1,5 +1,7 @@
+namespace test
 class inductive {u} is_equiv (A B : Type u) (f : A → B) : Type u
 definition inverse (A B : Type*) (f : A → B) [H : is_equiv A B f] := Type*
 definition foo (A : Type*) (B : A → Type*) (h : A → A) (g : Π(a : A), B a → B a)
                [H : Π(a : A), is_equiv _ _ (g a)] (x : A) : Type* :=
 inverse (B (h x)) (B (h x)) (g (h x))
+end test
diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean
index 83f19bf0c8..2a7f560631 100644
--- a/tests/lean/run/nat_bug.lean
+++ b/tests/lean/run/nat_bug.lean
@@ -1,4 +1,4 @@
-open decidable open eq
+open decidable
 namespace experiment
 inductive nat : Type
 | zero : nat
diff --git a/tests/lean/run/pred_using_structure_cmd.lean b/tests/lean/run/pred_using_structure_cmd.lean
index 37fc3aecbf..9216ebf0ed 100644
--- a/tests/lean/run/pred_using_structure_cmd.lean
+++ b/tests/lean/run/pred_using_structure_cmd.lean
@@ -2,7 +2,7 @@ variable {A : Type}
 
 structure has_refl (R : A → A → Prop) : Prop :=
 (refl : ∀ a, R a a)
-
+namespace test
 structure is_equiv (R : A → A → Prop) extends has_refl R : Prop :=
 (symm : ∀ a b, R a b → R b a)
 (trans : ∀ a b c, R a b → R b c → R a c)
@@ -11,3 +11,4 @@ structure is_equiv (R : A → A → Prop) extends has_refl R : Prop :=
 #check @is_equiv.symm
 #check @is_equiv.trans
 #check @is_equiv.to_has_refl
+end test
diff --git a/tests/lean/run/simp_univ_poly.lean b/tests/lean/run/simp_univ_poly.lean
index 52e0cea0ac..1daf5325ed 100644
--- a/tests/lean/run/simp_univ_poly.lean
+++ b/tests/lean/run/simp_univ_poly.lean
@@ -1,3 +1,4 @@
+namespace test
 universes u v
 
 def equinumerous (α : Type u) (β : Type v) :=
@@ -20,4 +21,5 @@ local infix ` ≈ ` := equinumerous
 @[simp] lemma sum_empty {α} : (α ⊕ empty) ≈ α := sorry
 
 -- rewriting `ulift empty` ==> `empty` changes the universe level
-example {α : Type u} : (α ⊕ ulift empty) ≈ α := by simp
\ No newline at end of file
+example {α : Type u} : (α ⊕ ulift empty) ≈ α := by simp
+end test