@@ -1,5 +1,7 @@
11module System
22
3+import Data.So
4+
35%include C "unistd.h"
46%default partial
57%access public export
@@ -62,7 +64,7 @@ time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
6264 pure t
6365
6466||| Specify interval to sleep for, must be in range [0, 1000000]
65−usleep : (i : Int) -> { auto prf : (i > 0 && i <= 1000000) = True } -> IO ()
67+usleep : (i : Int) -> { auto prf : So (i > 0 && i <= 1000000) } -> IO ()
6668usleep i = foreign FFI_C "usleep" (Int -> IO ()) i
6769
6870system : String -> IO Int