diff options
| author | Andreas Grois <andi@grois.info> | 2023-12-01 23:21:14 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2023-12-01 23:30:43 +0100 |
| commit | 24d7fab85b2eb1b7996fd0ceccdd0377f1ce087b (patch) | |
| tree | 2295b86307d2e5e6fbb59f009d84a635d74ef096 /Common/Option.lean | |
Day 1
Diffstat (limited to 'Common/Option.lean')
| -rw-r--r-- | Common/Option.lean | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Common/Option.lean b/Common/Option.lean new file mode 100644 index 0000000..23ea8d6 --- /dev/null +++ b/Common/Option.lean @@ -0,0 +1,7 @@ +namespace Option + +def zip (a : Option α) (b : Option β) : Option (α×β) := a >>= λ a ↦ b >>= λ b ↦ (a,b) + +def unzip : (a : Option (α×β)) → (Option α) × (Option β) +| none => (none, none) +| some (a, b) => (some a, some b) |