Add ability to desugar terms.

Remove `getChildren` construct---it's too niche for the core language.

1 files changed, 11 insertions, 0 deletions

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)