From b0d0cf973dec411fbcf53e423382738d97c122e6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 Jul 2019 17:44:25 -0700
Subject: [PATCH] chore(tests): fix tests

---
 tests/bench/rbmap.lean             |  2 +-
 tests/bench/rbmap2.lean            |  2 +-
 tests/bench/rbmap3.lean            | 16 ++++++++--------
 tests/bench/rbmap4.lean            |  2 +-
 tests/bench/rbmap_checkpoint.lean  |  2 +-
 tests/bench/rbmap_checkpoint2.lean |  6 +++---
 tests/lean/run/deriv.lean          |  2 +-
 tests/lean/run/handlers.lean       |  2 +-
 tests/lean/trust0/t1.lean          |  2 +-
 9 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/tests/bench/rbmap.lean b/tests/bench/rbmap.lean
index 7e58649cf3..c66ec7b353 100644
--- a/tests/bench/rbmap.lean
+++ b/tests/bench/rbmap.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.ordering.basic init.coe init.data.option.basic init.io
+import init.data.ordering.basic init.coe init.data.option.basic init.system.io
 
 universes u v w w'
 
diff --git a/tests/bench/rbmap2.lean b/tests/bench/rbmap2.lean
index b90acd7802..9f24530db1 100644
--- a/tests/bench/rbmap2.lean
+++ b/tests/bench/rbmap2.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.ordering.basic init.coe init.data.option.basic init.io
+import init.data.ordering.basic init.coe init.data.option.basic init.system.io
 
 universes u v w w'
 
diff --git a/tests/bench/rbmap3.lean b/tests/bench/rbmap3.lean
index 162875947a..3c10e4c19b 100644
--- a/tests/bench/rbmap3.lean
+++ b/tests/bench/rbmap3.lean
@@ -1,5 +1,5 @@
 prelude
-import init.core init.io init.data.ordering
+import init.core init.system.io init.data.ordering
 
 universes u v w
 
@@ -42,11 +42,11 @@ protected def max : Rbnode α β → Option (Sigma (fun k => β k))
 | leaf b               := b
 | (Node _ l k v r)   b := revFold l (f k v (revFold r b))
 
-@[specialize] def all (p : ∀ k : α, β k → Bool) : Rbnode α β → Bool
+@[specialize] def all (p : ∀ (k : α), β k → Bool) : Rbnode α β → Bool
 | leaf                 := true
 | (Node _ l k v r)     := p k v && all l && all r
 
-@[specialize] def any (p : ∀ k : α, β k → Bool) : Rbnode α β → Bool
+@[specialize] def any (p : ∀ (k : α), β k → Bool) : Rbnode α β → Bool
 | leaf               := false
 | (Node _ l k v r)   := p k v || any l || any r
 
@@ -103,10 +103,10 @@ def flipColors : ∀ (n : Rbnode α β), n ≠ leaf → Rbnode α β
 | leaf h := absurd rfl h
 
 def fixup (n : Rbnode α β) (h : n ≠ leaf) : Rbnode α β :=
-let n₁ := rotateLeft n h in
-let h₁ := (rotateLeftNeLeaf n h) in
-let n₂ := rotateRight n₁ h₁ in
-let h₂ := (rotateRightNeLeaf n₁ h₁) in
+let n₁ := rotateLeft n h;
+let h₁ := (rotateLeftNeLeaf n h);
+let n₂ := rotateRight n₁ h₁;
+let h₂ := (rotateRightNeLeaf n₁ h₁);
 flipColors n₂ h₂
 
 def setBlack : Rbnode α β → Rbnode α β
@@ -133,7 +133,7 @@ variable (lt : α → α → Prop)
 
 variable [DecidableRel lt]
 
-def findCore : Rbnode α β → ∀ k : α, Option (Sigma (fun k => β k))
+def findCore : Rbnode α β → ∀ (k : α), Option (Sigma (fun k => β k))
 | leaf                 x := none
 | (Node _ a ky vy b) x :=
   (match cmpUsing lt x ky with
diff --git a/tests/bench/rbmap4.lean b/tests/bench/rbmap4.lean
index 7e58649cf3..c66ec7b353 100644
--- a/tests/bench/rbmap4.lean
+++ b/tests/bench/rbmap4.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.ordering.basic init.coe init.data.option.basic init.io
+import init.data.ordering.basic init.coe init.data.option.basic init.system.io
 
 universes u v w w'
 
diff --git a/tests/bench/rbmap_checkpoint.lean b/tests/bench/rbmap_checkpoint.lean
index be612f81ba..74827a0eb8 100644
--- a/tests/bench/rbmap_checkpoint.lean
+++ b/tests/bench/rbmap_checkpoint.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.ordering.basic init.coe init.data.option.basic init.io
+import init.data.ordering.basic init.coe init.data.option.basic init.system.io
 
 universes u v w w'
 
diff --git a/tests/bench/rbmap_checkpoint2.lean b/tests/bench/rbmap_checkpoint2.lean
index dddd0ce493..365009be25 100644
--- a/tests/bench/rbmap_checkpoint2.lean
+++ b/tests/bench/rbmap_checkpoint2.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.ordering.basic init.coe init.data.option.basic init.io
+import init.data.ordering.basic init.coe init.data.option.basic init.system.io
 
 universes u v w w'
 
@@ -67,8 +67,8 @@ else ins t k v
 def mkMapAux (freq : Nat) : Nat → Tree → List Tree → List Tree
 | 0     m r := m::r
 | (n+1) m r :=
-  let m := insert m n (n % 10 = 0) in
-  let r := if n % freq == 0 then m::r else r in
+  let m := insert m n (n % 10 = 0);
+  let r := if n % freq == 0 then m::r else r;
   mkMapAux n m r
 
 def mkMap (n : Nat) (freq : Nat) : List Tree :=
diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean
index 85748a9e26..7e83b34cfd 100644
--- a/tests/lean/run/deriv.lean
+++ b/tests/lean/run/deriv.lean
@@ -1,5 +1,5 @@
 /- Benchmark for new code generator -/
-import init.io
+import init.system.io
 
 inductive Expr
 | Val : Int → Expr
diff --git a/tests/lean/run/handlers.lean b/tests/lean/run/handlers.lean
index 24014be6f5..df0b13f9b2 100644
--- a/tests/lean/run/handlers.lean
+++ b/tests/lean/run/handlers.lean
@@ -1,4 +1,4 @@
-import init.io
+import init.system.io
 
 #exit
 
diff --git a/tests/lean/trust0/t1.lean b/tests/lean/trust0/t1.lean
index d083d257d5..3ecd0162ca 100644
--- a/tests/lean/trust0/t1.lean
+++ b/tests/lean/trust0/t1.lean
@@ -1,2 +1,2 @@
-import init.io
+import init.system.io
 #print trust