diff options
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) |