diff options
| author | Andreas Grois <andi@grois.info> | 2023-12-07 21:53:19 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2023-12-07 21:53:19 +0100 |
| commit | e6f4111aa97f34383369577bff011d546d26d000 (patch) | |
| tree | b9990a0b7b1bc6c2b6a9684356656d5adb29f6b2 /Common/Option.lean | |
| parent | 8d6efb1c1fdddc1fbad167510ce25e56be684130 (diff) | |
Day 6
Diffstat (limited to 'Common/Option.lean')
| -rw-r--r-- | Common/Option.lean | 4 |
1 files changed, 4 insertions, 0 deletions
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 |