feat: add IO.toEIO

This commit is contained in:
Leonardo de Moura 2020-08-19 09:43:26 -07:00
parent e3b1ae514b
commit 9158ba60ea

View file

@ -45,6 +45,9 @@ abbrev IO : Type → Type := EIO IO.Error
@[inline] def EIO.toIO {α ε} (f : ε → IO.Error) (x : EIO ε α) : IO α :=
x.adaptExcept f
@[inline] def IO.toEIO {α ε} (f : IO.Error → ε) (x : IO α) : EIO ε α :=
x.adaptExcept f
section
/- After we inline `EState.run'`, the closed term `((), ())` is generated, where the second `()`
represents the "initial world". We don't want to cache this closed term. So, we disable