on master help sign in
Update type-providers-ffi.rst

making the code work with latest Idris version (1.2)

commit41951f21d64c486c27d5c2a949cf8a62f7217291 authorMichel Bøje Randahl Nielsen <michel@randahl.net> dateFri 23 Feb 2018, 23:40 (9 years ago) parent2be6e6a
1 file changed+3−1
docs/guides/type-providers-ffi.rst+3−1
docs/guides/type-providers-ffi.rst+3−1
@@ -200,6 +200,7 @@ Next, an Idris file to define our providers:
200200 module Providers
201201
202202 %dynamic "./stattypes.so"
203+ %access export
203204
204205 sizeOfDevT : IO Int
205206 sizeOfDevT = foreign FFI_C "sizeof_dev_t" (IO Int)
@@ -207,9 +208,10 @@ Next, an Idris file to define our providers:
207208
208209 -- Indicates how many bits are used to represent various system
209210 -- stat types.
211+ public export
210212 data BitWidth = B8 | B16 | B32 | B64
211213
212− implementation Show BitWidth where
214+ Show BitWidth where
213215 show B8 = "8 bits"
214216 show B16 = "16 bits"
215217 show B32 = "32 bits"