git.iko.soy/Idris-dev
on master help sign in
Used So instead of =
c9883e6Saurabh Rawat
libs/base/System.idr+3−1
compare with master
unifiedsplit
@@ -1,5 +1,7 @@
1module System
1module System
2
2
3+import Data.So
4+
3%include C "unistd.h"
5%include C "unistd.h"
4%default partial
6%default partial
5%access public export
7%access public export
@@ -62,7 +64,7 @@ time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
62 pure t
64 pure t
63
65
64||| Specify interval to sleep for, must be in range [0, 1000000]
66||| 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 ()
66usleep i = foreign FFI_C "usleep" (Int -> IO ()) i
68usleep i = foreign FFI_C "usleep" (Int -> IO ()) i
67
69
68system : String -> IO Int
70system : String -> IO Int