@@ -17,17 +17,12 @@ import IO
17%access public export
17%access public export
19||| A file handle
19||| A file handle
21data File : Type where
20data File : Type where
22 FHandle : (p : Ptr) -> File
21 FHandle : (p : Ptr) -> File
24-- Usage hints for erasure analysis
23-- Usage hints for erasure analysis
25%used FHandle p
24%used FHandle p
27−||| Pointer to a C FILE structure (for passing to C routines)
31||| An error from a file operation
26||| An error from a file operation
32-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
27-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
33-- the values correspond!
28-- the values correspond!