From a9230817da88305b16d658a056e72bef159b8f94 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 11 Sep 2024 13:59:17 +0100
Subject: Define terms.

---
 src/Data/Maybe/Decidable.idr | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 src/Data/Maybe/Decidable.idr

(limited to 'src/Data')

diff --git a/src/Data/Maybe/Decidable.idr b/src/Data/Maybe/Decidable.idr
new file mode 100644
index 0000000..e301ab1
--- /dev/null
+++ b/src/Data/Maybe/Decidable.idr
@@ -0,0 +1,6 @@
+module Data.Maybe.Decidable
+
+public export
+data OnlyWhen : (p : a -> Type) -> Maybe a -> Type where
+  RJust : forall x. (px : p x) -> p `OnlyWhen` Just x
+  RNothing : (false : (x : a) -> Not (p x)) -> p `OnlyWhen` Nothing
-- 
cgit v1.2.3