From 124637c9468c3876b3da35e977f90b3a5e7c9885 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 24 Jun 2023 14:28:08 +0200
Subject: [PATCH] add SnocVect.select

---
 lib/Quox/Thin/View.idr | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/lib/Quox/Thin/View.idr b/lib/Quox/Thin/View.idr
index 912001d..59a5269 100644
--- a/lib/Quox/Thin/View.idr
+++ b/lib/Quox/Thin/View.idr
@@ -3,6 +3,7 @@ module Quox.Thin.View
 import public Quox.Thin.Base
 import Quox.NatExtra
 import Data.Singleton
+import Data.SnocVect
 
 %default total
 
@@ -90,3 +91,13 @@ export
              view (Keep {mask} ope eq) = KeepV mask ope
 viewKeep ope eq with (view (Keep ope eq))
   viewKeep ope Refl | KeepV _ ope = Refl
+
+
+namespace SnocVect
+  export
+  select : {n, mask : Nat} -> (0 ope : OPE m n mask) ->
+           SnocVect n a -> SnocVect m a
+  select ope sx with (view ope)
+    select _ [<]       | StopV       = [<]
+    select _ (sx :< x) | DropV _ ope = select ope sx
+    select _ (sx :< x) | KeepV _ ope = select ope sx :< x