@@ -1,6 +1,6 @@
1module System
1module System
3−import Data.So
3+import public Data.So
5%include C "unistd.h"
5%include C "unistd.h"
6%default partial
6%default partial
@@ -93,7 +93,8 @@ time : IO Integer
93time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
93time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
96+||| Specify interval to sleep for, must be in range [0, 1000000]
96−usleep : Int -> IO ()
97+usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> IO ()
97usleep i = foreign FFI_C "usleep" (Int -> IO ()) i
98usleep i = foreign FFI_C "usleep" (Int -> IO ()) i
99system : String -> IO Int
100system : String -> IO Int