diff options
| -rw-r--r-- | src/Core/Term.idr | 11 |
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) |