From d10e08236fb3bdaefd101bc2dc00e3c036895a3f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 9 Nov 2019 07:28:12 -0800
Subject: [PATCH] feat: add `finally`

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

diff --git a/library/Init/Control/Except.lean b/library/Init/Control/Except.lean
index d74d92ca43..69e423915d 100644
--- a/library/Init/Control/Except.lean
+++ b/library/Init/Control/Except.lean
@@ -184,3 +184,9 @@ instance (ε m out) [MonadRun out m] : MonadRun (fun α => out (Except ε α)) (
 -- useful for implicit failures in do-notation
 instance (m : Type → Type) [Monad m] : MonadFail (ExceptT String m) :=
 ⟨fun _ => throw⟩
+
+/-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
+@[inline] def finally {ε α β : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) (finalizer : m β) : m α :=
+catch
+  (do a ← x; finalizer; pure a)
+  (fun e => do finalizer; throw e)