Remove %error_reverse from IO'
%error_reverse needs a better implementation, until then it should be
used with care otherwise it might rewrite some things that it really
shouldn't!
commit5e94bc948d1350240a6cff58488a42591033c34b
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 2 Nov 2015, 14:38 (11 years ago)
parenteb041bc
libs/prelude/IO.idr−1
@@ -36,7 +36,6 @@ record FFI where
3636||| The IO type, parameterised over the FFI that is available within
3737||| it.
3838abstract
39−%error_reverse
4039data IO' : (lang : FFI) -> Type -> Type where
4140 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
4241