From 5f83999f483e241158706522a35364ba32f7f203 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 15 Apr 2023 16:16:35 +0100
Subject: Define Term substitution.

---
 src/Core/Thinning.idr | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'src/Core/Thinning.idr')

diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
index dc4efcb..a2500e9 100644
--- a/src/Core/Thinning.idr
+++ b/src/Core/Thinning.idr
@@ -68,3 +68,18 @@ export
 wkn : Fin m -> m `Thins` n -> Fin n
 wkn i IsId = i
 wkn i (IsThinner thin) = wkn' i thin
+
+-- Composition -----------------------------------------------------------------
+
+comp : Thinner m n -> Thinner k m -> Thinner k n
+comp IsBase thin2 = IsDrop thin2
+comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
+comp (IsKeep thin1) IsBase = IsDrop thin1
+comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
+comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)
+
+export
+(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
+IsId . thin2 = thin2
+IsThinner thin1 . IsId = IsThinner thin1
+IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)
-- 
cgit v1.2.3