From ecaf9deb4b1d2ce85617438e621690b2df3ea367 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 12 Nov 2024 16:44:31 +0000
Subject: Add ability to desugar terms.

Remove `getChildren` construct---it's too niche for the core language.
---
 src/Inky/Data/SnocList/Thinning.idr | 11 +++++++++++
 1 file changed, 11 insertions(+)

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

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
@@ -96,6 +97,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
-- 
cgit v1.2.3