git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3107 from colin-adams/file-c-ptr
b87820dNiklas Larsson
libs/prelude/Prelude/File.idr−1
compare with master
unifiedsplit
@@ -17,7 +17,6 @@ import IO
17%access public export
17%access public export
18
18
19||| A file handle
19||| A file handle
20−export
21data File : Type where
20data File : Type where
22 FHandle : (p : Ptr) -> File
21 FHandle : (p : Ptr) -> File
23
22