diff options
Diffstat (limited to 'Common')
| -rw-r--r-- | Common/Option.lean | 7 |
1 files changed, 7 insertions, 0 deletions
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 · ·) |