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),