From e258c78a5ab9529242b4c8fa168eda85430e641e Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 28 Oct 2024 15:34:16 +0000 Subject: Make everything relevant. Too few proofs were relevant. Now they are. --- src/Inky/Data/Irrelevant.idr | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 src/Inky/Data/Irrelevant.idr (limited to 'src/Inky/Data/Irrelevant.idr') 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) -- cgit v1.2.3