From e6f4111aa97f34383369577bff011d546d26d000 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Thu, 7 Dec 2023 21:53:19 +0100
Subject: Day 6

---
 Common/Option.lean | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Common/Option.lean')

diff --git a/Common/Option.lean b/Common/Option.lean
index 23ea8d6..275f83f 100644
--- a/Common/Option.lean
+++ b/Common/Option.lean
@@ -5,3 +5,7 @@ def zip (a : Option α) (b : Option β) : Option (α×β) := a >>= λ a ↦ b >>
 def unzip : (a : Option (α×β)) → (Option α) × (Option β)
 | none => (none, none)
 | some (a, b) => (some a, some b)
+
+def toExcept {α : Type u0} {ε : Type u1} { m : Type u0 → Type u2} [Pure m] [MonadExcept m (ε := ε)] (error : ε) : Option α → m α
+| none => throw error
+| some a => pure a
-- 
cgit v1.2.3