From 6ce6cf4580f2c0ab4c7c4ec56f438c1cc184c7cd Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 12 Nov 2024 18:05:25 +0000
Subject: Add more names. Names are good.

---
 src/Inky/Data/SnocList/Quantifiers.idr | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

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

diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
index ac6287b..886c4e4 100644
--- a/src/Inky/Data/SnocList/Quantifiers.idr
+++ b/src/Inky/Data/SnocList/Quantifiers.idr
@@ -3,7 +3,6 @@ module Inky.Data.SnocList.Quantifiers
 import public Data.SnocList.Quantifiers
 
 import Data.List.Quantifiers
-import Inky.Data.Irrelevant
 import Inky.Data.SnocList
 import Inky.Data.SnocList.Elem
 import Inky.Decidable
@@ -26,22 +25,14 @@ 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 :
+  ((x : a) -> LazyEither (p x) (q x)) ->
+  (sx : SnocList a) -> LazyEither (All p sx) (Any q 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
 tabulate : LengthOf sx -> (forall x. Elem x sx -> p x) -> All p sx
 tabulate Z f = [<]
-- 
cgit v1.2.3