From 2a16b5832463955359762f407b03c1090de39319 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 May 2016 14:23:57 -0700
Subject: [PATCH] test(tests/lean/run): add another IO test

---
 library/system/IO.lean  |  2 +-
 tests/lean/run/IO2.lean | 13 +++++++++++++
 2 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/IO2.lean

diff --git a/library/system/IO.lean b/library/system/IO.lean
index 3c7c3c7f2d..42a9020a21 100644
--- a/library/system/IO.lean
+++ b/library/system/IO.lean
@@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch and Leonardo de Moura
 -/
-constant IO : Type → Type₁
+constant IO : Type → Type
 constant functorIO : functor IO
 constant monadIO : monad IO
 
diff --git a/tests/lean/run/IO2.lean b/tests/lean/run/IO2.lean
new file mode 100644
index 0000000000..5f47717f67
--- /dev/null
+++ b/tests/lean/run/IO2.lean
@@ -0,0 +1,13 @@
+import system.IO data.list
+open list
+
+/- B and unit must be in the same universe
+   So, we must put B at Type₁ or use poly_unit
+   since unit is at Type₁
+-/
+
+definition for {A : Type} {B : Type} : list A → (A → IO B) → IO poly_unit
+| []      f := return poly_unit.star
+| (x::xs) f := do f x, for xs f
+
+vm_eval for [1,2,3,4,5] (λ i, do put_str "value: ", put_nat i, put_str "\n")