From e258c78a5ab9529242b4c8fa168eda85430e641e Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 28 Oct 2024 15:34:16 +0000
Subject: Make everything relevant.

Too few proofs were relevant. Now they are.
---
 src/Inky/Data/SnocList/Quantifiers.idr | 46 ++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 src/Inky/Data/SnocList/Quantifiers.idr

(limited to 'src/Inky/Data/SnocList/Quantifiers.idr')

diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
new file mode 100644
index 0000000..73c6551
--- /dev/null
+++ b/src/Inky/Data/SnocList/Quantifiers.idr
@@ -0,0 +1,46 @@
+module Inky.Data.SnocList.Quantifiers
+
+import public Data.SnocList.Quantifiers
+
+import Data.List.Quantifiers
+import Inky.Data.Irrelevant
+import Inky.Decidable
+
+public export
+(<><) : All p xs -> All p sx -> All p (xs <>< sx)
+sxp <>< [] = sxp
+sxp <>< (px :: pxs) = (sxp :< px) <>< pxs
+
+public export
+head : All p (sx :< x) -> p x
+head (prfs :< px) = px
+
+public export
+tail : All p (sx :< x) -> All p sx
+tail (prfs :< px) = prfs
+
+public export
+HSnocList : SnocList Type -> Type
+HSnocList = All id
+
+public export
+all : ((x : a) -> Dec' (p x)) -> (sx : SnocList a) -> LazyEither (All p sx) (Any (Not . p) sx)
+all f [<] = True `Because` [<]
+all f (sx :< x) =
+  map (\prfs => snd prfs :< fst prfs) (either Here There) $
+  both (f x) (all f sx)
+
+public export
+irrelevant : {0 sx : SnocList a} -> All (Irrelevant . p) sx -> Irrelevant (All p sx)
+irrelevant [<] = Forget [<]
+irrelevant (prfs :< px) = [| irrelevant prfs :< px |]
+
+public export
+relevant : (sx : SnocList a) -> (0 prfs : All p sx) -> All (Irrelevant . p) sx
+relevant [<] _ = [<]
+relevant (sx :< x) prfs = relevant sx (tail prfs) :< Forget (head prfs)
+
+public export
+data Pairwise : (a -> a -> Type) -> SnocList a -> Type where
+  Lin : Pairwise r [<]
+  (:<) : Pairwise r sx -> All (flip r x) sx -> Pairwise r (sx :< x)
-- 
cgit v1.2.3