From 66cd4c57cf98df8385cbdbb0960b7400fee98350 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 11 Apr 2017 17:32:03 +0200 Subject: [PATCH] feat(library/system/io): alternative instance for io --- library/system/io.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/library/system/io.lean b/library/system/io.lean index d45e9a52b5..1145d83dc6 100644 --- a/library/system/io.lean +++ b/library/system/io.lean @@ -92,6 +92,14 @@ interface.iterate e α a f def forever {e} (a : io_core e unit) : io_core e unit := 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 + +instance : alternative io := +{ interface.monad _ with + orelse := λ _ a b, catch a (λ _, b), + failure := λ _, io.fail "failure" } + def put_str : string → io unit := interface.term.put_str