From ce546fe96974cb7aa3b09c729f33ac6ba5169299 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 10 Jul 2023 13:37:56 +0100
Subject: Describe unification.

---
 src/Data/Maybe/Properties.idr | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/Data/Maybe/Properties.idr')

diff --git a/src/Data/Maybe/Properties.idr b/src/Data/Maybe/Properties.idr
index 99a3507..459cb8f 100644
--- a/src/Data/Maybe/Properties.idr
+++ b/src/Data/Maybe/Properties.idr
@@ -18,6 +18,11 @@ export
 extractIsJust : {x : Maybe a} -> (0 _ : IsJust x) -> (y ** x = Just y)
 extractIsJust ItIsJust = (_ ** Refl)
 
+%inline
+export
+extractIsNothing : {x : Maybe a} -> (0 _ : IsNothing x) -> x = Nothing
+extractIsNothing ItIsNothing = Refl
+
 %inline
 export
 mapIsJust : (0 f : a -> b) -> IsJust x -> IsJust (map f x)
-- 
cgit v1.2.3