Fix up issues relating to changes in Idris.
commit0a4aac7883c212748dc8856fb66da861a45940de
authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk>
dateSat 26 Mar 2016, 19:26 (11 years ago)
parent5700147
test/tutorial007/Providers.idr+4−1
@@ -1,13 +1,16 @@
11module Providers
22
3+%access export
4+
35%dynamic "./nativetypes.so"
46
57sizeOfSizeT : IO Int
68sizeOfSizeT = foreign FFI_C "sizeof_size_t" (IO Int)
79
10+public export
811data NativeTypeSize = OneByte | TwoBytes | FourBytes | EightBytes
912
10−instance Show NativeTypeSize where
13+Show NativeTypeSize where
1114 show OneByte = "1 byte"
1215 show TwoBytes = "2 bytes"
1316 show FourBytes = "4 bytes"
test/tutorial007/tutorial007.idr+2−1
@@ -1,11 +1,12 @@
11module Main
22import Providers
3+
34%language TypeProviders
45%provide (szSizeT : NativeTypeSize) with getSizeOfSizeT
56
67main : IO ()
78main = do
8− expected <- readFile "sizefromc.txt"
9+ (Right expected) <- readFile "sizefromc.txt" | (Left err) => printLn err
910 putStrLn $ if show szSizeT == expected
1011 then "Pass"
1112 else "Fail: \"" ++ show szSizeT ++ "\" /= \"" ++ expected ++ "\""