From 287a669f17359c696f3d2f588d9be658aafca51a Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Fri, 31 Mar 2023 17:54:08 +0100 Subject: Define Term weakening. --- src/Core/Term.idr | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src/Core') 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) -- cgit v1.2.3