Added to_C to Prelude.File
commit1f14478ae1085d9c1570795f29873ffd9e78f57d
authorColin Adams <colinpauladams@gmail.com>
dateSat 9 Apr 2016, 16:22 (11 years ago)
parent4079f54
libs/prelude/Prelude/File.idr+4
@@ -24,6 +24,10 @@ data File : Type where
2424-- Usage hints for erasure analysis
2525%used FHandle p
2626
27+||| Pointer to a C FILE structure (for passing to C routines)
28+to_C : File -> Ptr
29+to_C (FHandle p) = p
30+
2731||| An error from a file operation
2832-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
2933-- the values correspond!