Merge pull request #2491 from ziman/ffi-fix
Make `FFI_Exportable` usable with other back-ends
commit546458e0d68c641699f691d4c77ca03e4431f739
authorNiklas Larsson <metaniklas@gmail.com>
dateFri 31 Jul 2015, 13:12 (11 years ago)
parentd05f550098656e
libs/prelude/IO.idr+1−1
@@ -253,7 +253,7 @@ namespace FFI_Export
253253 %used FFI_Prim prim
254254
255255 data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
256− FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)
256+ FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO' f t)
257257 FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
258258 FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t
259259