@@ -253,7 +253,7 @@ namespace FFI_Export
253 %used FFI_Prim prim
253 %used FFI_Prim prim
255 data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
255 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)
257 FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
257 FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
258 FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t
258 FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t