3 files changed, 24 insertions, 0 deletions
diff --git a/src/Inky/Data/SnocList/Elem.idr b/src/Inky/Data/SnocList/Elem.idr
index 465e92c..c1e69f6 100644
--- a/src/Inky/Data/SnocList/Elem.idr
+++ b/src/Inky/Data/SnocList/Elem.idr
@@ -8,6 +8,7 @@ import Data.Singleton
 import Inky.Decidable
 import Inky.Decidable.Maybe
 import Inky.Data.Assoc
+import Inky.Data.List
 import Inky.Data.SnocList
 
 export
@@ -71,6 +72,11 @@ split Z pos = Left pos
 split (S len) Here = Right Here
 split (S len) (There pos) = mapSnd There $ split len pos
 
+public export
+wknL' : Elem x sx -> LengthOf xs -> Elem x (sx <>< xs)
+wknL' i Z = i
+wknL' i (S len) = wknL' (There i) len
+
 -- Lookup ----------------------------------------------------------------------
 
 export
diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
index 73c6551..ac6287b 100644
--- a/src/Inky/Data/SnocList/Quantifiers.idr
+++ b/src/Inky/Data/SnocList/Quantifiers.idr
@@ -4,6 +4,8 @@ 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
 
 public export
@@ -41,6 +43,11 @@ 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 = [<]
+tabulate (S len) f = tabulate len (f . There) :< f Here
+
+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)
diff --git a/src/Inky/Data/SnocList/Thinning.idr b/src/Inky/Data/SnocList/Thinning.idr
index f766069..60666d2 100644
--- a/src/Inky/Data/SnocList/Thinning.idr
+++ b/src/Inky/Data/SnocList/Thinning.idr
@@ -2,6 +2,7 @@ module Inky.Data.SnocList.Thinning
 
 import Data.DPair
 import Data.Nat
+import Inky.Data.List
 import Inky.Data.SnocList
 import Inky.Data.SnocList.Var
 import Inky.Data.SnocList.Quantifiers
@@ -97,6 +98,16 @@ prf.index ((%%) n {pos}) = irrelevantEq $ toVarCong $ toNatInjective $ prf.index
 -- Useful for Parsers ----------------------------------------------------------
 
 public export
+(<><) : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 <>< bound `Thins` ctx2 <>< bound
+f <>< Z = f
+f <>< S len = Keep f <>< len
+
+public export
+dropFish : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 `Thins` ctx2 <>< bound
+dropFish f Z = f
+dropFish f (S len) = dropFish (Drop f) len
+
+public export
 dropPos : (pos : Elem x ctx) -> dropElem ctx pos `Thins` ctx
 dropPos Here = Drop Id
 dropPos (There pos) = Keep (dropPos pos)