Make everything relevant.

Too few proofs were relevant. Now they are.

1 files changed, 19 insertions, 0 deletions

diff --git a/src/Inky/Data/Irrelevant.idr b/src/Inky/Data/Irrelevant.idr
new file mode 100644
index 0000000..ca72470
--- /dev/null
+++ b/src/Inky/Data/Irrelevant.idr
@@ -0,0 +1,19 @@
+module Inky.Data.Irrelevant
+
+public export
+record Irrelevant (a : Type) where
+  constructor Forget
+  0 value : a
+
+public export
+Functor Irrelevant where
+  map f x = Forget (f x.value)
+
+public export
+Applicative Irrelevant where
+  pure x = Forget x
+  f <*> x = Forget (f.value x.value)
+
+public export
+Monad Irrelevant where
+  join x = Forget (x.value.value)