diff options
Diffstat (limited to 'src/Core/Term.idr')
| -rw-r--r-- | src/Core/Term.idr | 12 |
1 files changed, 12 insertions, 0 deletions
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) |