max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: generalize IO.sleep to BaseIO

Browse source
This commit is contained in:
Gabriel Ebner 2022-07-19 20:15:28 +02:00 • committed by Leonardo de Moura
parent 553addc078
commit 22c3ec3996
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/System/IO.lean
View file

@ -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