Exported FHandle to facilitate passing Files to and from C
commit567729e240df36d54dc088540393bdfd3241ece5
authorColin Adams <colinpauladams@gmail.com>
dateSun 10 Apr 2016, 06:41 (11 years ago)
parent1f14478
libs/prelude/Prelude/File.idr−5
@@ -17,17 +17,12 @@ import IO
1717%access public export
1818
1919||| A file handle
20−export
2120data File : Type where
2221 FHandle : (p : Ptr) -> File
2322
2423-- Usage hints for erasure analysis
2524%used FHandle p
2625
27−||| Pointer to a C FILE structure (for passing to C routines)
28−to_C : File -> Ptr
29−to_C (FHandle p) = p
30−
3126||| An error from a file operation
3227-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
3328-- the values correspond!