chore(tests/lean): fix test suite

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

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)

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

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

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

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.
 

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

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

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

tests/lean/run/nat_bug.lean

@@ -1,4 +1,4 @@
-open decidable open eq
+open decidable
 namespace experiment
 inductive nat : Type
 | zero : nat

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

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
+example {α : Type u} : (α ⊕ ulift empty) ≈ α := by simp
+end test