From 85828629146596817d1a4a37b5642160bb9bb3e8 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 6 Nov 2022 13:03:54 +0100
Subject: [PATCH] remove stdlib duplication

---
 lib/Quox/OPE/Basics.idr | 11 -----------
 lib/Quox/OPE/Sub.idr    | 10 ++++++++++
 2 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/lib/Quox/OPE/Basics.idr b/lib/Quox/OPE/Basics.idr
index d4d92fc..b462a24 100644
--- a/lib/Quox/OPE/Basics.idr
+++ b/lib/Quox/OPE/Basics.idr
@@ -9,14 +9,3 @@ Scope = SnocList
 public export
 Scoped : Type -> Type
 Scoped a = Scope a -> Type
-
-public export
-data All : (a -> Type) -> Scoped a where
-  Lin  : All p [<]
-  (:<) : All p xs -> p x -> All p (xs :< x)
-%name OPE.Basics.All ps, qs
-
-public export
-mapAll : (forall x. p x -> q x) -> All p xs -> All q xs
-mapAll f [<]      = [<]
-mapAll f (x :< y) = mapAll f x :< f y
diff --git a/lib/Quox/OPE/Sub.idr b/lib/Quox/OPE/Sub.idr
index de7e2b2..71f92d1 100644
--- a/lib/Quox/OPE/Sub.idr
+++ b/lib/Quox/OPE/Sub.idr
@@ -5,6 +5,7 @@ import Quox.OPE.Length
 import Quox.NatExtra
 import Data.DPair
 import Data.SnocList.Elem
+import Data.SnocList.Quantifiers
 
 %default total
 
@@ -99,12 +100,21 @@ export
 appZeroRight {len = Z} p = Refl
 
 
+||| if `p` holds for all elements of the main list,
+||| it holds for all elements of the sublist
 public export
 subAll : xs `Sub` ys -> All p ys -> All p xs
 subAll End      [<]       = [<]
 subAll (Keep q) (ps :< x) = subAll q ps :< x
 subAll (Drop q) (ps :< x) = subAll q ps
 
+||| if `p` holds for one element of the sublist,
+||| it holds for one element of the main list
+public export
+subAny : xs `Sub` ys -> Any p xs -> Any p ys
+subAny (Keep q) (Here  x) = Here x
+subAny (Keep q) (There x) = There (subAny q x)
+subAny (Drop q) x         = There (subAny q x)
 
 
 public export