From a6e5f7c0c830308c3912a043d4e741a13d3ce6cd Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 8 Sep 2024 17:00:18 +0200
Subject: Begin implementing Day10 Part1

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

(limited to 'Common/Option.lean')

diff --git a/Common/Option.lean b/Common/Option.lean
index 275f83f..9344d83 100644
--- a/Common/Option.lean
+++ b/Common/Option.lean
@@ -9,3 +9,10 @@ def unzip : (a : Option (α×β)) → (Option α) × (Option β)
 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
+
+def bindWithProof (o : Option α) (f : (v : α) → (o = some v) → Option β) : Option β :=
+  match o with
+  | .some v => f v rfl
+  | .none => none
+
+def mapWithProof (o : Option α) (f : (v : α) → (o = some v) → β) : Option β := bindWithProof o (some $ f · ·)
-- 
cgit v1.2.3