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 ++++++++++++
 1 file changed, 12 insertions(+)

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

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)
-- 
cgit v1.2.3