Merge pull request #3548 from eklavya/master
Restrict System.usleep interval
commit1da1805a2e097aef23fcc181a97236eeeb35cf54
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateThu 12 Jan 2017, 21:51 (10 years ago)
parenta7c7eb158fc44e
libs/base/System.idr+3−2
@@ -1,6 +1,6 @@
11module System
22
3−import Data.So
3+import public Data.So
44
55%include C "unistd.h"
66%default partial
@@ -93,7 +93,8 @@ time : IO Integer
9393time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
9494 pure t
9595
96−usleep : Int -> IO ()
96+||| Specify interval to sleep for, must be in range [0, 1000000]
97+usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> IO ()
9798usleep i = foreign FFI_C "usleep" (Int -> IO ()) i
9899
99100system : String -> IO Int