Make everything relevant.

Too few proofs were relevant. Now they are.

1 files changed, 46 insertions, 0 deletions

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)