ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 14:38:20 +03:00
Code Issues Projects Releases Wiki Activity

Make FFI_Exportable more generic.

Browse Source
This commit is contained in:
Matus Tejiscak 2015-07-31 00:50:03 +01:00
parent 8ed600091f
commit 098656e423
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/prelude/IO.idr
View File

@ -226,7 +226,7 @@ namespace FFI_Export
%used FFI_Prim prim
data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)
FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO' f t)
FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t