diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-14 17:47:22 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-14 17:47:22 +0100 |
| commit | ed9beabb1e5f867bad0c0693f36cd0ffc0d5d96c (patch) | |
| tree | d7a3a2029b037f51878d0d6256d9436c854af841 /src/Core/Term.idr | |
| parent | fe1f03b7cd7cfeb9992a968b5a5cbebe8fbe9b7d (diff) | |
Define weakening.
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) |