chore(tests): fix tests

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'
 

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'
 

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

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'
 

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'
 

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 :=

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

tests/lean/run/handlers.lean

@@ -1,4 +1,4 @@
-import init.io
+import init.system.io
 
 #exit
 

tests/lean/trust0/t1.lean

@@ -1,2 +1,2 @@
-import init.io
+import init.system.io
 #print trust