git.iko.soy/Idris-dev
on master help sign in
Remove %error_reverse from IO'
5e94bc9Edwin Brady
libs/prelude/IO.idr−1
compare with master
unifiedsplit
@@ -36,7 +36,6 @@ record FFI where
36||| The IO type, parameterised over the FFI that is available within
36||| The IO type, parameterised over the FFI that is available within
37||| it.
37||| it.
38abstract
38abstract
39−%error_reverse
40data IO' : (lang : FFI) -> Type -> Type where
39data IO' : (lang : FFI) -> Type -> Type where
41 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
40 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
42
41