Define Term weakening.

1 files changed, 11 insertions, 0 deletions

diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index 603d8a9..ee61c88 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -2,6 +2,7 @@ module Core.Term
 
 import Core.Context
 import Core.Var
+import Core.Thinning
 
 %prefix_record_projections off
 
@@ -18,3 +19,13 @@ data Term : Context -> Type where
   App : Term sx -> Term sx -> Term sx
 
 %name Term t, u, v
+
+-- Operations ------------------------------------------------------------------
+
+public export
+wkn : Term sx -> sx `Thins` sy -> Term sy
+wkn (Var i) thin = Var $ wkn i thin
+wkn Set thin = Set
+wkn (Pi n t u) thin = Pi n (wkn t thin) (wkn u $ keep thin n)
+wkn (Abs n t) thin = Abs n (wkn t $ keep thin n)
+wkn (App t u) thin = App (wkn t thin) (wkn u thin)