From 9158ba60ea75b7eb6121d80dddff2dd3ffe806bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 19 Aug 2020 09:43:26 -0700
Subject: [PATCH] feat: add `IO.toEIO`

---
 src/Init/System/IO.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index d960eacb24..a2b87b9bf6 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -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