From ed9beabb1e5f867bad0c0693f36cd0ffc0d5d96c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 14 Apr 2023 17:47:22 +0100
Subject: Define weakening.

---
 src/Core/Term.idr     | 12 ++++++++++++
 src/Core/Thinning.idr | 15 +++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index 7fea482..1b050ca 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -1,5 +1,7 @@
 module Core.Term
 
+import Core.Thinning
+
 import public Data.Fin
 
 -- Definition ------------------------------------------------------------------
@@ -15,3 +17,13 @@ data Term : Nat -> Type where
   App : Term n -> Term n -> Term n
 
 %name Term t, u, v
+
+-- Weakening -------------------------------------------------------------------
+
+public export
+wkn : Term m -> m `Thins` n -> Term n
+wkn (Var i) thin = Var (wkn i thin)
+wkn Set thin = Set
+wkn (Pi t u) thin = Pi (wkn t thin) (wkn u $ keep thin)
+wkn (Abs t) thin = Abs (wkn t $ keep thin)
+wkn (App t u) thin = App (wkn t thin) (wkn u thin)
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
index 0067ac4..dc4efcb 100644
--- a/src/Core/Thinning.idr
+++ b/src/Core/Thinning.idr
@@ -1,5 +1,7 @@
 module Core.Thinning
 
+import Data.Fin
+
 -- Definition ------------------------------------------------------------------
 
 data Thinner : Nat -> Nat -> Type where
@@ -53,3 +55,16 @@ view IsId = Id m
 view (IsThinner IsBase) = Drop (id _)
 view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
 view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
+
+-- Weakening -------------------------------------------------------------------
+
+wkn' : Fin m -> Thinner m n -> Fin n
+wkn' i IsBase = FS i
+wkn' i (IsDrop thin) = FS (wkn' i thin)
+wkn' FZ (IsKeep thin) = FZ
+wkn' (FS i) (IsKeep thin) = FS (wkn' i thin)
+
+export
+wkn : Fin m -> m `Thins` n -> Fin n
+wkn i IsId = i
+wkn i (IsThinner thin) = wkn' i thin
-- 
cgit v1.2.3