From c4aef89296f1a5a44bfb9cd76b2693ebdbc96980 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 4 May 2017 07:57:42 +0200
Subject: [PATCH] feat(system/io): add finally combinator

---
 library/system/io.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/library/system/io.lean b/library/system/io.lean
index f2aed01582..f108bad347 100644
--- a/library/system/io.lean
+++ b/library/system/io.lean
@@ -100,6 +100,14 @@ iterate () $ λ _, a >> return (some ())
 def catch {e₁ e₂ α} (a : io_core e₁ α) (b : e₁ → io_core e₂ α) : io_core e₂ α :=
 interface.catch e₁ e₂ α a b
 
+def finally {α e} (a : io_core e α) (cleanup : io_core e unit) : io_core e α := do
+res ← catch (sum.inr <$> a) (return ∘ sum.inl),
+cleanup,
+match res with
+| sum.inr res := return res
+| sum.inl error := io.interface.fail _ _ error
+end
+
 instance : alternative io :=
 { interface.monad _ with
   orelse := λ _ a b, catch a (λ _, b),