From d8d7eba6c53d15fad042dd331de8b75712228ece Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 9 Nov 2021 16:53:24 +0100
Subject: [PATCH] feat: liftExcept

---
 src/Init/Control/Except.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 01554eb2d5..c0a42c1fa4 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -135,6 +135,10 @@ end MonadExcept
 @[inline] def observing {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) : m (Except ε α) :=
   tryCatch (do let a ← x; pure (Except.ok a)) (fun ex => pure (Except.error ex))
 
+def liftExcept [MonadExceptOf ε m] [Pure m] : Except ε α → m α
+  | Except.ok a    => pure a
+  | Except.error e => throw e
+
 instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m) where
   stM        := Except ε
   liftWith f := liftM <| f fun x => x.run