From 22c3ec39968994cd7aaf3bb0d80445e6fa7e827a Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 19 Jul 2022 20:15:28 +0200
Subject: [PATCH] chore: generalize `IO.sleep` to `BaseIO`

---
 src/Init/System/IO.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index d6d4268c5a..2c8160cf46 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -172,7 +172,7 @@ def lazyPure (fn : Unit → α) : IO α :=
 If `nBytes = 0`, return immediately with an empty buffer. -/
 @[extern "lean_io_get_random_bytes"] opaque getRandomBytes (nBytes : USize) : IO ByteArray
 
-def sleep (ms : UInt32) : IO Unit :=
+def sleep (ms : UInt32) : BaseIO Unit :=
   -- TODO: add a proper primitive for IO.sleep
   fun s => dbgSleep ms fun _ => EStateM.Result.ok () s