From d4ebcc04ce96bd2ad4a6185ec3c86bc460beef29 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <patrick@patrickstevens.co.uk>
Date: Sun, 15 Sep 2019 15:08:51 +0100
Subject: [PATCH] Couple of useful Maybe functions (#44)

---
 Maybe.agda | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Maybe.agda b/Maybe.agda
index f7bef86..0452905 100644
--- a/Maybe.agda
+++ b/Maybe.agda
@@ -31,3 +31,9 @@ module Maybe where
   defaultValue : {a : _} → {A : Set a} → (default : A) → Maybe A → A
   defaultValue default no = default
   defaultValue default (yes x) = x
+
+  noNotYes : {a : _} {A : Set a} {b : A} → (no ≡ yes b) → False
+  noNotYes ()
+
+  mapMaybePreservesNo : {a b : _} {A : Set a} {B : Set b} (f : A → B) (x : Maybe A) → mapMaybe f x ≡ no → x ≡ no
+  mapMaybePreservesNo f no pr = refl