From 919007612a7b6f8cec1b5c801d6b9c7e84bfec2b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 22 Nov 2014 17:34:05 -0800
Subject: [PATCH] fix(tests/lean): adjust tests since module 'logic' depends on
 nat

We need that because of the definitional package
---
 tests/lean/run/algebra1.lean      |  4 +++-
 tests/lean/run/class4.lean        |  3 ++-
 tests/lean/run/class5.lean        | 15 ++++++++-------
 tests/lean/run/coe7.lean          |  3 ++-
 tests/lean/run/coe8.lean          |  2 +-
 tests/lean/run/nat_bug.lean       |  3 ++-
 tests/lean/run/nat_bug2.lean      |  3 ++-
 tests/lean/run/nat_bug3.lean      |  3 ++-
 tests/lean/run/nat_bug4.lean      |  3 ++-
 tests/lean/run/nat_bug5.lean      |  3 ++-
 tests/lean/run/nat_bug6.lean      |  3 ++-
 tests/lean/run/nat_bug7.lean      |  3 ++-
 tests/lean/run/nat_coe.lean       |  3 ++-
 tests/lean/run/over_subst.lean    |  3 ++-
 tests/lean/run/tactic23.lean      |  3 ++-
 tests/lean/run/uni.lean           |  3 ++-
 tests/lean/run/uni2.lean          |  3 ++-
 tests/lean/run/uni_issue1.lean    |  3 ++-
 tests/lean/slow/nat_bug1.lean     |  2 ++
 tests/lean/slow/nat_bug2.lean     |  3 ++-
 tests/lean/slow/nat_wo_hints.lean |  2 ++
 21 files changed, 48 insertions(+), 25 deletions(-)

diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index dec2c3244..457abe94a 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -1,5 +1,6 @@
 import logic
 
+namespace experiment
 definition Type1 := Type.{1}
 
 context
@@ -49,7 +50,7 @@ namespace nat
   := algebra.add_struct.mk add
 
   definition to_nat (n : num) : nat
-  := #algebra
+  := #experiment.algebra
     num.rec nat.zero (λ n, pos_num.rec (succ zero) (λ n r, r + r) (λ n r, r + r + succ zero) n) n
 end nat
 
@@ -111,3 +112,4 @@ section
   check a*b*c*a*b*c*a*b*a*b*c*a
   check a*b
 end
+end experiment
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index 0d03db227..d2b918736 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -1,5 +1,5 @@
 import logic
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -90,3 +90,4 @@ reducible [off] add
 check dvd a (a + (succ b))
 
 end nat
+end experiment
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index f38cea46a..23a89b7f6 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -1,5 +1,5 @@
 import logic
-
+namespace experiment
 namespace algebra
   inductive mul_struct [class] (A : Type) : Type :=
   mk : (A → A → A) → mul_struct A
@@ -33,7 +33,7 @@ end
 section
   open [notation] algebra
   open nat
-  -- check mul_struct nat  << This is an error, we are open only the notation from algebra
+  -- check mul_struct nat  << This is an error, we opened only the notation from algebra
   variables a b c : nat
   check a * b * c
   definition tst2 : nat := a * b * c
@@ -41,10 +41,10 @@ end
 
 section
   open nat
-  -- check mul_struct nat  << This is an error, we are open only the notation from algebra
+  -- check mul_struct nat  << This is an error, we opened only the notation from algebra
   variables a b c : nat
-  check #algebra a*b*c
-  definition tst3 : nat := #algebra a*b*c
+  check a*b*c
+  definition tst3 : nat := #nat a*b*c
 end
 
 section
@@ -54,6 +54,7 @@ section
   := algebra.mul_struct.mk add
 
   variables a b c : nat
-  check #algebra a*b*c  -- << is open add instead of mul
-  definition tst4 : nat := #algebra a*b*c
+  check #experiment.algebra a*b*c  -- << is open add instead of mul
+  definition tst4 : nat := #experiment.algebra a*b*c
 end
+end experiment
diff --git a/tests/lean/run/coe7.lean b/tests/lean/run/coe7.lean
index 7e04f300b..fda2f4f3b 100644
--- a/tests/lean/run/coe7.lean
+++ b/tests/lean/run/coe7.lean
@@ -1,5 +1,5 @@
 import logic
-
+namespace experiment
 constant nat : Type.{1}
 constant int : Type.{1}
 constant of_nat : nat → int
@@ -9,3 +9,4 @@ theorem tst (n : nat) : n = n :=
 have H : true, from trivial,
 calc n    = n : eq.refl _
       ... = n : eq.refl _
+end experiment
diff --git a/tests/lean/run/coe8.lean b/tests/lean/run/coe8.lean
index 510491854..d58eb7db8 100644
--- a/tests/lean/run/coe8.lean
+++ b/tests/lean/run/coe8.lean
@@ -1,5 +1,5 @@
 import logic
-
+namespace experiment
 constant nat : Type.{1}
 constant int : Type.{1}
 constant of_nat : nat → int
diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean
index 15a66dfcb..4fc773f97 100644
--- a/tests/lean/run/nat_bug.lean
+++ b/tests/lean/run/nat_bug.lean
@@ -1,7 +1,7 @@
 import logic
 open decidable
 open eq
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -24,3 +24,4 @@ theorem zero_or_succ2 (n : nat) : n = zero ∨ n = succ (pred n)
     (take m IH, or.intro_right _
       (show succ m = succ (pred (succ m)), from congr_arg succ (symm (pred_succ m))))
 end nat
+end experiment
diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean
index 864ecf419..ee29522d7 100644
--- a/tests/lean/run/nat_bug2.lean
+++ b/tests/lean/run/nat_bug2.lean
@@ -1,6 +1,6 @@
 import logic
 open eq.ops
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -23,3 +23,4 @@ theorem succ_le {n m : nat} (H : n ≤ m) : succ n ≤ succ m
 := add_one m ▸ add_one n ▸ add_le_right H 1
 
 end nat
+end experiment
diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean
index 98a05aeef..83b5b1540 100644
--- a/tests/lean/run/nat_bug3.lean
+++ b/tests/lean/run/nat_bug3.lean
@@ -1,6 +1,6 @@
 import logic
 open eq.ops
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -23,3 +23,4 @@ theorem succ_le_cancel {n m : nat} (H : succ n ≤ succ m) :  n ≤ m
 := add_le_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H)
 
 end nat
+end experiment
diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean
index a197e11f7..5aca421c3 100644
--- a/tests/lean/run/nat_bug4.lean
+++ b/tests/lean/run/nat_bug4.lean
@@ -1,6 +1,6 @@
 import logic
 open eq.ops
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -15,3 +15,4 @@ open eq
 theorem small2 (n m l : nat) : n * succ l + m = n * l + n + m
 := subst (mul_succ_right _ _) (eq.refl (n * succ l + m))
 end nat
+end experiment
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index 9d22b020a..597e16759 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -1,6 +1,6 @@
 import logic
 open eq.ops eq
-
+namespace foo
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -33,3 +33,4 @@ theorem mul_add_distr_left (n m k : nat) : (n + m) * k = n * k + m * k
           ... = n * succ l + (m * l + m) : {symm (mul_succ_right _ _)}
           ... = n * succ l + m * succ l : {symm (mul_succ_right _ _)})
 end nat
+end foo
diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean
index 7279386a0..261dffd87 100644
--- a/tests/lean/run/nat_bug6.lean
+++ b/tests/lean/run/nat_bug6.lean
@@ -1,6 +1,6 @@
 import logic
 open eq.ops
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -19,3 +19,4 @@ print "==========================="
 theorem tst (n : nat) (H : P (n * zero)) : P zero
 := eq.subst (mul_zero_right _) H
 end nat
+exit
diff --git a/tests/lean/run/nat_bug7.lean b/tests/lean/run/nat_bug7.lean
index fb9a9ae0d..b59f7297a 100644
--- a/tests/lean/run/nat_bug7.lean
+++ b/tests/lean/run/nat_bug7.lean
@@ -1,5 +1,5 @@
 import logic
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -14,3 +14,4 @@ print "==========================="
 theorem bug (a b c d : nat) : a + b + c + d = a + c + b + d
 := subst (add_right_comm _ _ _) (eq.refl (a + b + c + d))
 end nat
+end experiment
diff --git a/tests/lean/run/nat_coe.lean b/tests/lean/run/nat_coe.lean
index bdd89cf52..2696d2161 100644
--- a/tests/lean/run/nat_coe.lean
+++ b/tests/lean/run/nat_coe.lean
@@ -1,5 +1,5 @@
 import logic
-
+namespace experiment
 constant nat : Type.{1}
 constant int : Type.{1}
 
@@ -24,3 +24,4 @@ definition c2 := i + j
 
 theorem T2 : c2 = int_add i j :=
 eq.refl _
+exit
diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean
index 79365cfb0..b211b8abf 100644
--- a/tests/lean/run/over_subst.lean
+++ b/tests/lean/run/over_subst.lean
@@ -1,5 +1,5 @@
 import logic
-
+namespace experiment
 namespace nat
 constant nat : Type.{1}
 constant add : nat → nat → nat
@@ -29,3 +29,4 @@ open nat
 open eq
 theorem add_lt_left {a b : int} (H : a < b) (c : int) : c + a < c + b :=
 subst (symm (add_assoc c a one)) (add_le_left H c)
+end experiment
diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean
index 656f48ed9..2c5e0b526 100644
--- a/tests/lean/run/tactic23.lean
+++ b/tests/lean/run/tactic23.lean
@@ -1,5 +1,5 @@
 import logic
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -35,3 +35,4 @@ theorem T2 : ∃ a, (is_zero a) = true
 := by apply exists_intro; apply eq.refl
 
 end nat
+end experiment
diff --git a/tests/lean/run/uni.lean b/tests/lean/run/uni.lean
index a02a76f29..1011cf462 100644
--- a/tests/lean/run/uni.lean
+++ b/tests/lean/run/uni.lean
@@ -1,5 +1,5 @@
 import logic
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -46,3 +46,4 @@ end
 test_unify(env, t(m), tt, 1)
 test_unify(env, t(m), ff, 1)
 *)
+end experiment
diff --git a/tests/lean/run/uni2.lean b/tests/lean/run/uni2.lean
index acb773229..625e03a50 100644
--- a/tests/lean/run/uni2.lean
+++ b/tests/lean/run/uni2.lean
@@ -1,5 +1,5 @@
 import logic
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -48,3 +48,4 @@ end
 
 test_unify(env, f(t(m)), f(tt), 1)
 *)
+exit
diff --git a/tests/lean/run/uni_issue1.lean b/tests/lean/run/uni_issue1.lean
index adb8ac83c..8aceff03d 100644
--- a/tests/lean/run/uni_issue1.lean
+++ b/tests/lean/run/uni_issue1.lean
@@ -1,8 +1,9 @@
 import logic
-
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
 
 definition is_zero (n : nat)
 := nat.rec true (λ n r, false) n
+end experiment
diff --git a/tests/lean/slow/nat_bug1.lean b/tests/lean/slow/nat_bug1.lean
index a15172d50..2527de427 100644
--- a/tests/lean/slow/nat_bug1.lean
+++ b/tests/lean/slow/nat_bug1.lean
@@ -6,6 +6,7 @@
 import logic
 open tactic
 
+namespace foo
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -23,3 +24,4 @@ print "=================="
 theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x :=
 eq.refl _
 end nat
+end foo
diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean
index ec841c33a..496ce74c7 100644
--- a/tests/lean/slow/nat_bug2.lean
+++ b/tests/lean/slow/nat_bug2.lean
@@ -6,7 +6,7 @@
 import logic algebra.binary
 open tactic binary eq.ops eq
 open decidable
-
+namespace experiment
 definition refl := @eq.refl
 definition and_intro := @and.intro
 definition or_intro_left := @or.intro_left
@@ -1410,3 +1410,4 @@ theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m
       ... = dist l m : dist_add_left k l m
 
 end nat
+end experiment
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index e4950d608..98501af2e 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -7,6 +7,7 @@ import logic algebra.binary
 open tactic binary eq.ops eq
 open decidable
 
+namespace experiment
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
@@ -1415,3 +1416,4 @@ theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m
 
 
 end nat
+end experiment