Make FFI_Exportable more generic.
commit098656e4233235ad66db167e2cc571e4e8e4181d
authorMatus Tejiscak <ziman@functor.sk>
dateFri 31 Jul 2015, 00:50 (11 years ago)
parent8ed6000
libs/prelude/IO.idr+1−1
@@ -226,7 +226,7 @@ namespace FFI_Export
226226 %used FFI_Prim prim
227227
228228 data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
229− FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)
229+ FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO' f t)
230230 FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
231231 FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t
232232